exponentExists — Mathlib

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

Похожие утверждения