card_eq_or_dvd — Mathlib

English

For a p-group G, either the group is trivial (card = 1) or p divides the cardinal of G.

Русский

Для p-группы G либо она тривиальна (кардар 1), либо p делит кардинал G.

LaTeX

$$$\IsPGroup(p,G) \rightarrow [Fact(p.Prime)] \rightarrow Nat.card G = 1 \;\lor\; p \mid Nat.card G$$$

Lean4

theorem card_eq_or_dvd : Nat.card G = 1 ∨ p ∣ Nat.card G :=
  by
  cases finite_or_infinite G
  · obtain ⟨n, hn⟩ := iff_card.mp hG
    rw [hn]
    rcases n with - | n
    · exact Or.inl rfl
    · exact Or.inr ⟨p ^ n, by rw [pow_succ']⟩
  · rw [Nat.card_eq_zero_of_infinite]
    exact Or.inr ⟨0, rfl⟩

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