Commit 2025-03-05 11:44 3212de11

View on Github →

feat(GroupTheory/OrderOfElement): add IsConj.isOfFinOrder (#22507) Upstreamed from the EquationalTheories project. Adds the lemma IsConj.isOfFinOrder that finite order is invariant under conjugation. In order to prove this for general monoids, there are small adjustments in Algebra/Group/Conj: IsConj.pow is added and isConj_one_right / isConj_one_left are promoted from cancellative monoids to general monoids.

Estimated changes

added theorem IsConj.pow
modified theorem isConj_one_right
added theorem IsUnit.mul_eq_left
added theorem IsUnit.mul_eq_right
added theorem IsConj.isOfFinOrder