Commit 2024-02-23 11:29 1afb2fb3

feat(GroupTheory/Exponent): lemmas around Monoid.exponent and Subgroup/Submonoid (#10598) Proves some helpful properties of Monoid.exponent on Submonoid G and Subgroup G:

• the exponent of a group is equal to 1 iff the monoid is trivial (previously only the reverse implication was proven)
• the exponent of G divides the exponent of H if there exists a multiplication-preserving injection from G to H
• Monoid.exponent G = Monoid.exponent H if G ≃* H
• Monoid.exponent ⊤ = Monoid.exponent G
• g ^ Monoid.exponent H = 1 if g ∈ H
• generalizes one_lt_exponent to LeftCancelMonoid