English
If there exists a multiplicative equivalence between G and H, then the exponent of G equals the exponent of H.
Русский
Если существует эквивалентность умножения между G и H, то экспонента G равна экспоненте H.
LaTeX
$$$\\operatorname{exponent} G = \\operatorname{exponent} H$$$
Lean4
/-- If there exists a multiplication-preserving equivalence between `G` and `H`,
then the exponent of `G` is equal to the exponent of `H`.
-/
@[to_additive /-- If there exists a addition-preserving equivalence between `G` and `H`,
then the exponent of `G` is equal to the exponent of `H`. -/
]
theorem exponent_eq_of_mulEquiv (e : G ≃* H) : Monoid.exponent G = Monoid.exponent H :=
Nat.dvd_antisymm (exponent_dvd_of_monoidHom e e.injective) (exponent_dvd_of_monoidHom e.symm e.symm.injective)
