English
The exponent of the additive version of a group equals the exponent of the original monoid.
Русский
Экспонента аддитивной версии группы равна экспоненте исходного моноида.
LaTeX
$$$\\operatorname{exponent}(\\mathrm{Additive}\\,G)=\\operatorname{exponent}(G)$$$
Lean4
/-- The exponent of a group is the smallest positive integer `n` such that `g ^ n = 1` for all
`g ∈ G` if it exists, otherwise it is zero by convention. -/
@[to_additive /-- The exponent of an additive group is the smallest positive integer `n` such that
`n • g = 0` for all `g ∈ G` if it exists, otherwise it is zero by convention. -/
]
noncomputable def exponent :=
if h : ExponentExists G then Nat.find h else 0
