English
For finite groups, IsPGroup p G is equivalent to |G| = p^n for some n.
Русский
Для конечной группы IsPGroup p G эквивалентно |G| = p^n для некоторого n.
LaTeX
$$IsPGroup p G ↔ ∃ n, Nat.card G = p^n$$
Lean4
theorem iff_card [Fact p.Prime] [Finite G] : IsPGroup p G ↔ ∃ n : ℕ, Nat.card G = p ^ n :=
by
have hG : Nat.card G ≠ 0 := Nat.card_pos.ne'
refine ⟨fun h => ?_, fun ⟨n, hn⟩ => of_card hn⟩
suffices ∀ q ∈ (Nat.card G).primeFactorsList, q = p
by
use (Nat.card G).primeFactorsList.length
rw [← List.prod_replicate, ← List.eq_replicate_of_mem this, Nat.prod_primeFactorsList hG]
intro q hq
obtain ⟨hq1, hq2⟩ := (Nat.mem_primeFactorsList hG).mp hq
haveI : Fact q.Prime := ⟨hq1⟩
obtain ⟨g, hg⟩ := exists_prime_orderOf_dvd_card' q hq2
obtain ⟨k, hk⟩ := (iff_orderOf.mp h) g
exact (hq1.pow_eq_iff.mp (hg.symm.trans hk).symm).1.symm
