inv_eq_self_of_orderOf_eq_two

Mathlib.GroupTheory.Exponent

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

← MathLib Explorer

English

If orderOf x = 2 then x^{-1} = x.

Русский

Если orderOf x = 2, тогда x^{-1} = x.

LaTeX

$$$\operatorname{orderOf}(x)=2 \Rightarrow x^{-1}=x$$$

Lean4

/-- If an element in a group has order two, then it is its own inverse. -/
@[to_additive]
theorem inv_eq_self_of_orderOf_eq_two {x : G} (hx : orderOf x = 2) : x⁻¹ = x :=
  inv_eq_of_mul_eq_one_left <| pow_two (a := x) ▸ hx ▸ pow_orderOf_eq_one x

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

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

Разделы

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

Аффилиация

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