pow_card_eq_one

Mathlib.GroupTheory.OrderOfElement

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

← MathLib Explorer

English

For any finite group G and element x, x^{|G|} = 1, i.e., the order divides the group order.

Русский

Если |G| — порядок группы, то x^{|G|} = 1 для любого x ∈ G.

LaTeX

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

Lean4

@[to_additive (attr := simp) card_nsmul_eq_zero]
theorem pow_card_eq_one : x ^ Fintype.card G = 1 := by rw [← Nat.card_eq_fintype_card, pow_card_eq_one']

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

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

Разделы

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

Аффилиация

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