English
For a finite generated abelian group G, the order of G divides exponent(G) raised to rank(G): |G| | exponent(G)^{rank(G)}.
Русский
Для конечно порожденной абелевой группы G порядок делит экспоненту G в степени ранга G: |G| | exponent(G)^{rank(G)}.
LaTeX
$$$ |G| \mid \operatorname{exponent}(G)^{\operatorname{rank} G} $$$
Lean4
@[to_additive]
theorem card_dvd_exponent_pow_rank : Nat.card G ∣ Monoid.exponent G ^ Group.rank G := by
classical
obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
rw [← hS1, ← Fintype.card_coe, ← Finset.card_univ, ← Finset.prod_const]
let f : (∀ g : S, zpowers (g : G)) →* G := noncommPiCoprod fun s t _ x y _ _ => mul_comm x _
have hf : Function.Surjective f :=
by
rw [← MonoidHom.range_eq_top, eq_top_iff, ← hS2, closure_le]
exact fun g hg => ⟨Pi.mulSingle ⟨g, hg⟩ ⟨g, mem_zpowers g⟩, noncommPiCoprod_mulSingle _ _⟩
replace hf := card_dvd_of_surjective f hf
rw [Nat.card_pi] at hf
refine hf.trans (Finset.prod_dvd_prod_of_dvd _ _ fun g _ => ?_)
rw [Nat.card_zpowers]
exact Monoid.order_dvd_exponent (g : G)
