IsPGroup

Mathlib.GroupTheory.PGroup

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

English

A p-group is a group in which every element has order p^k for some k ∈ ℕ.

Русский

p-группа — это группа, в которой каждый элемент имеет порядок p^k для некоторого k ∈ ℕ.

LaTeX

$$IsPGroup p G := ∀ g ∈ G, ∃ k ∈ ℕ, g^{p^k} = 1$$

Lean4

/-- A p-group is a group in which every element has prime power order -/
def IsPGroup : Prop :=
  ∀ g : G, ∃ k : ℕ, g ^ p ^ k = 1

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

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

Разделы

Аффилиация

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