inv_eq_self_of_exponent_two — Mathlib

English

In a group with exponent two, every element is its own inverse: x^{-1} = x.

Русский

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

LaTeX

$$$\operatorname{exponent} G = 2 \Rightarrow \forall x \in G, x^{-1} = x$$$

Lean4

/-- In a group of exponent two, every element is its own inverse. -/
@[to_additive]
theorem inv_eq_self_of_exponent_two (hG : Monoid.exponent G = 2) (x : G) : x⁻¹ = x :=
  inv_eq_of_mul_eq_one_left <| pow_two (a := x) ▸ hG ▸ Monoid.pow_exponent_eq_one x

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