mul_self

Mathlib.GroupTheory.SpecificGroups.KleinFour

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

English

In a Klein four group, every element satisfies x^2 = e.

Русский

В Klein Four для каждого элемента выполняется x^2 = e.

LaTeX

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

Lean4

@[to_additive]
theorem mul_self (x : G) : x * x = 1 := by rw [mul_eq_one_iff_eq_inv, inv_eq_self]

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

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

Разделы

Аффилиация

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