coreflection_apply_self — Mathlib

English

The coreflection is its own inverse when acting on coroots; applying it twice yields the original coroot.

Русский

Действие coreflection над корротом обратно: дважды применить — вернуть исходный коррот.

LaTeX

$$$ (P.coreflection(i))(P.coroot(j)) = P.coroot(j) $$$

Lean4

@[simp]
theorem coreflection_apply_self : P.coreflection i (P.coroot i) = -P.coroot i :=
  Module.reflection_apply_self (P.flip.coroot_root_two i)

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