exponent_eq_card — Mathlib

English

Same as above: for a finite Z-group, exponent equals the order of G.

Русский

То же: для конечной Z-группы экспонента равна порядку группы.

LaTeX

$$$ \operatorname{exponent}(G) = |G| $ for finite Z-group G.$$

Lean4

theorem exponent_eq_card [Finite G] [IsZGroup G] : Monoid.exponent G = Nat.card G :=
  by
  refine dvd_antisymm Group.exponent_dvd_nat_card ?_
  rw [← Nat.factorization_prime_le_iff_dvd Nat.card_pos.ne' Monoid.exponent_ne_zero_of_finite]
  intro p hp
  have := Fact.mk hp
  let P : Sylow p G := default
  rw [← hp.pow_dvd_iff_le_factorization Monoid.exponent_ne_zero_of_finite, ← P.card_eq_multiplicity, ←
    (isZGroup p hp P).exponent_eq_card]
  exact Monoid.exponent_dvd_of_monoidHom P.1.subtype P.1.subtype_injective

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