Commit 2024-10-27 08:54 89bb4c76

View on Github →

refactor: generalise the Ruzsa triangle inequality to non-abelian groups (#18145) The proof works just fine, and the other statements too, up to turning some * around. Add supporting lemmas of the form op '' (s * t) = op '' t * op '' s. Use the new # notation for Finset.card.

Estimated changes