coreflection_apply_left — Mathlib

English

If IsOrthogonal i j, then coreflection j applied to coroot i equals coroot i: P.coreflection j (P.coroot i) = P.coroot i.

Русский

Если i и j ортогональны, то корефлекция j сохраняет корот i: P.coreflection j (P.coroot i) = P.coroot i.

LaTeX

$$$$ P.coreflection_j( P.coroot_i ) = P.coroot_i. $$$$

Lean4

theorem coreflection_apply_left (h : IsOrthogonal P i j) : P.coreflection j (P.coroot i) = P.coroot i :=
  h.flip.reflection_apply_left

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