involution — Mathlib

English

For any RingInvo R and x ∈ R, applying the involution twice returns the original element: (f (f x).unop).unop = x.

Русский

Для кольцевой инволюции RingInvo R и любого x ∈ R при двойном применении инволюции получаем исходное x.

LaTeX

$$$\forall f:\mathrm{RingInvo}(R),\ \forall x\in R:\ (f(f(x)).\mathrm{unop}).\mathrm{unop} = x$$$

Lean4

@[simp]
theorem involution (f : RingInvo R) (x : R) : (f (f x).unop).unop = x :=
  f.involution' x

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