inv_eq_self

Mathlib.GroupTheory.SpecificGroups.KleinFour

URI: https://scilib.ai/kg/mathlib#IsKleinFour.inv_eq_self

English

In a Klein four group, every element is its own inverse: x^{-1} = x for all x.

Русский

В группе Klein Four каждый элемент является своим обратным: x^{-1} = x.

LaTeX

$$x^{-1} = x \quad \text{for all } x\in G$$

Lean4

@[to_additive]
theorem inv_eq_self (x : G) : x⁻¹ = x :=
  inv_eq_self_of_exponent_two (by simp) x

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

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

Разделы

Аффилиация

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