nontrivial_iff_card — Mathlib

English

For a finite p-group, Nontrivial G iff there exists n>0 with |G| = p^n.

Русский

Для конечной p-группы G эквивалентно: существует n>0 такое, что |G| = p^n.

LaTeX

$$$\IsPGroup(p,G) \rightarrow [Fact(p.Prime)] [Finite G] \rightarrow (Nontrivial G) \leftrightarrow \exists n>0, Nat.card G = p^n$$$

Lean4

theorem nontrivial_iff_card [Finite G] : Nontrivial G ↔ ∃ n > 0, Nat.card G = p ^ n :=
  ⟨fun hGnt =>
    let ⟨k, hk⟩ := iff_card.1 hG
    ⟨k, Nat.pos_of_ne_zero fun hk0 => by rw [hk0, pow_zero] at hk; exact Finite.one_lt_card.ne' hk, hk⟩,
    fun ⟨_, hk0, hk⟩ =>
    Finite.one_lt_card_iff_nontrivial.1 <| hk.symm ▸ one_lt_pow₀ (Fact.out (p := p.Prime)).one_lt (ne_of_gt hk0)⟩

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