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
.