reflection_apply_root — Mathlib

English

The reflection of the j-th root by i is the root j diminished by the pairing between j and i times the i-th root.

Русский

Отражение по i-му корню действуем над корнем j: отражение по i переведёт корень j в корень j минус парирование(j,i) умноженное на корень i.

LaTeX

$$$ P.reflection(i)(P.root(j)) = P.root(j) - (P.pairing(j,i)) \cdot P.root(i) $$$

Lean4

theorem reflection_apply_root : P.reflection i (P.root j) = P.root j - (P.pairing j i) • P.root i :=
  rfl

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