Product theorem

[YaelDillies]

Let $n \ge 0$. There are $\delta, \epsilon > 0$ such that for any field $k$ and any finite symmetric generating subset $A \subseteq SL_n(k)$ we have $|A^3| \ge |A|^{1 + \delta}$ or $|A| \ge |G|^{1 - \epsilon}$.

This is Theorems 1.9 and 5.1 in the lecture notes and theorem_1_9 in the Lean code.