reflection_same — Mathlib

English

The reflection map is its own inverse; applying it twice yields the identity.

Русский

Отражение является собственной обратной функцией: дважды применение даёт тождественное отображение.

LaTeX

$$$ (P.reflection(i))^{-1} = P.reflection(i) $$$

Lean4

@[simp]
theorem reflection_same (x : M) : P.reflection i (P.reflection i x) = x :=
  Module.involutive_reflection (P.coroot_root_two i) x

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