two_mul_apply_root_root — Mathlib

English

For all i, j, the identity 2 · B.form (P.root i) (P.root j) equals pairing i j times B.form (P.root j) (P.root j) holds.

Русский

Для всех i, j выполняется тождество 2 · B.form (P.root i) (P.root j) = pairing i j · B.form (P.root j) (P.root j).

LaTeX

$$$ 2 \\cdot B.form\\bigl(P.root\\ i\\bigr)\\bigl(P.root\\ j\\bigr) = P.pairing\\ i\\ j \\cdot B.form\\bigl(P.root\\ j\\ bigr)\\bigl(P.root\\ j\\bigr) $$$

Lean4

theorem two_mul_apply_root_root : 2 * B.form (P.root i) (P.root j) = P.pairing i j * B.form (P.root j) (P.root j) :=
  by
  rw [two_mul, ← eq_sub_iff_add_eq]
  nth_rw 1 [← B.isOrthogonal_reflection j]
  rw [reflection_apply, reflection_apply_self, root_coroot'_eq_pairing, LinearMap.map_sub₂, LinearMap.map_smul₂,
    smul_eq_mul, LinearMap.map_neg, LinearMap.map_neg, mul_neg, neg_sub_neg]

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