pow_exponent_eq_one

Mathlib.GroupTheory.Exponent

URI: https://scilib.ai/kg/mathlib#Monoid.pow_exponent_eq_one

← MathLib Explorer

English

For any g ∈ G, g^{exponent(G)} = 1 holds.

Русский

Для любого g ∈ G выполняется g^{exponent(G)} = 1.

LaTeX

$$$g^{\\operatorname{exponent}(G)}=1$$$

Lean4

@[to_additive exponent_nsmul_eq_zero]
theorem pow_exponent_eq_one (g : G) : g ^ exponent G = 1 := by
  classical
  by_cases h : ExponentExists G
  · simp_rw [exponent, dif_pos h]
    exact (Nat.find_spec h).2 g
  · simp_rw [exponent, dif_neg h, pow_zero]

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

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

Разделы

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

Аффилиация

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