iff_orderOf — Mathlib

English

For a prime p, IsPGroup p G is equivalent to: for all g ∈ G there exists k with orderOf(g) = p^k.

Русский

Для простого p, IsPGroup p G эквивалентно: для каждого g ∈ G существует k с orderOf(g) = p^k.

LaTeX

$$IsPGroup p G ↔ ∀ g ∈ G, ∃ k ∈ ℕ, orderOf(g) = p^k$$

Lean4

theorem iff_orderOf [hp : Fact p.Prime] : IsPGroup p G ↔ ∀ g : G, ∃ k : ℕ, orderOf g = p ^ k :=
  forall_congr' fun g =>
    ⟨fun ⟨_, hk⟩ => Exists.imp (fun _ h => h.right) ((Nat.dvd_prime_pow hp.out).mp (orderOf_dvd_of_pow_eq_one hk)),
      Exists.imp fun k hk => by rw [← hk, pow_orderOf_eq_one]⟩

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