English
If all elements have positive order, then exponent G ≠ 0 iff the range of orderOf is finite.
Русский
Если у всех элементов положительный порядок, то экспонента G ≠ 0 тогда и только тогда диапазон orderOf конечен.
LaTeX
$$$(\\\\forall g : G, 0 < \\\\operatorname{orderOf} g) \\\\Rightarrow \\\\operatorname{exponent} G \\\\neq 0 \\\\iff \\\\operatorname{Set.range}(\\\\operatorname{orderOf} : G \\\\to \\\\mathbb{N}).\\\\Finite$$$
Lean4
@[to_additive]
theorem exponent_ne_zero_iff_range_orderOf_finite (h : ∀ g : G, 0 < orderOf g) :
exponent G ≠ 0 ↔ (Set.range (orderOf : G → ℕ)).Finite :=
by
refine ⟨fun he => ?_, fun he => ?_⟩
· by_contra h
obtain ⟨m, ⟨t, rfl⟩, het⟩ := Set.Infinite.exists_gt h (exponent G)
exact pow_ne_one_of_lt_orderOf he het (pow_exponent_eq_one t)
· lift Set.range (orderOf (G := G)) to Finset ℕ using he with t ht
have htpos : 0 < t.prod id := by
refine Finset.prod_pos fun a ha => ?_
rw [← Finset.mem_coe, ht] at ha
obtain ⟨k, rfl⟩ := ha
exact h k
suffices exponent G ∣ t.prod id by
intro h
rw [h, zero_dvd_iff] at this
exact htpos.ne' this
rw [exponent_dvd]
intro g
apply Finset.dvd_prod_of_mem id (?_ : orderOf g ∈ _)
rw [← Finset.mem_coe, ht]
exact Set.mem_range_self g
