Commit 2024-10-21 21:50 13d0934b
View on Github →feat: ‖aba⁻¹b⁻¹ - 1‖ ≤ C ‖a - 1‖ ‖b - 1‖ (#18027)
for a, b invertible. This will used to show the Breuillard-Green-Tao theorem in the case of matrices, which will then be bootstrapped to the full Breuillard-Green-Tao theorem.
From GrowthInGroups (LeanCamCombi)