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.