coroot_reflectionPerm — Mathlib

English

The coreflection of a coroot j is the coroot j minus pairing(i,j) times the coroot i.

Русский

Отражение-coreflection корота j равно короту j минус pairing(i,j) умноженное на корот i.

LaTeX

$$$ P.coreflection(i)(P.coroot(j)) = P.coroot(j) - (P.pairing(i,j)) \cdot P.coroot(i) $$$

Lean4

@[simp]
theorem coroot_reflectionPerm (j : ι) : P.coroot (P.reflectionPerm i j) = (P.coreflection i) (P.coroot j) :=
  (P.reflectionPerm_coroot i j).symm

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