English
The group exponent exists for any bounded torsion group.
Русский
Существование экспоненты-возможности для любой ограниченной торсионной группы.
LaTeX
$$$IsTorsion(G) \wedge \text{bounded}(G) \Rightarrow ExponentExists(G)$$$
Lean4
/-- The group exponent exists for any bounded torsion group. -/
@[to_additive IsAddTorsion.exponentExists /-- The group exponent exists for any bounded additive torsion group. -/
]
theorem exponentExists (tG : IsTorsion G) (bounded : (Set.range fun g : G => orderOf g).Finite) : ExponentExists G :=
exponent_ne_zero.mp <| (exponent_ne_zero_iff_range_orderOf_finite fun g => (tG g).orderOf_pos).mpr bounded