pow_card_eq_one'

Mathlib.GroupTheory.OrderOfElement

URI: https://scilib.ai/kg/mathlib#pow_card_eq_one'

← MathLib Explorer

English

In any finite group G, the nth power of any element x satisfies x^{|G|} = 1.

Русский

В любой конечной группе G для любого элемента x выполняется x^{|G|} = 1.

LaTeX

$$$x^{\operatorname{card}(G)} = 1$$$

Lean4

@[to_additive (attr := simp) card_nsmul_eq_zero']
theorem pow_card_eq_one' {G : Type*} [Group G] {x : G} : x ^ Nat.card G = 1 :=
  orderOf_dvd_iff_pow_eq_one.mp <| orderOf_dvd_natCard _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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