of_card

Mathlib.GroupTheory.PGroup

URI: https://scilib.ai/kg/mathlib#IsPGroup.of_card

English

If |G| = p^n, then G is a p-group.

Русский

Если кардинал группы G равен p^n, то G является p-группой.

LaTeX

$$|G| = p^n ⇒ IsPGroup p G$$

Lean4

theorem of_card {n : ℕ} (hG : Nat.card G = p ^ n) : IsPGroup p G := fun g => ⟨n, by rw [← hG, pow_card_eq_one']⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru