Commit 2026-01-09 11:59 1f3b5da5
View on Github →refactor: unify the two versions of pow_eq_one_iff (#30799)
One version is about torsion-free monoids, the other one about linearly ordered monoids. I argue that all linearly ordered monoids of interest are torsion-free, and therefore the correct lemma to keep is the former.
As a byproduct, I must move a few MonoidHom lemmas.
Zulip