of_bot

Mathlib.GroupTheory.PGroup

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

English

The trivial subgroup is a p-group.

Русский

Тривиальная подгруппа является p-группой.

LaTeX

$$IsPGroup p (⊥ : Subgroup G)$$

Lean4

theorem of_bot : IsPGroup p (⊥ : Subgroup G) :=
  of_card (n := 0) (by rw [Subgroup.card_bot, pow_zero])

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

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

Разделы

Аффилиация

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