English
The product over all a of RootForm(P.root a)(P.root a) times coroot i lies in the range of Polarization.domRestrict(rootSpan).
Русский
Произведение RootForm(P.root a)(P.root a) по всем a умноженное на корoot i лежит в диапазоне Polarization.domRestrict(rootSpan).
LaTeX
$$($\\prod_{a\\in ι} P.RootForm (P.root a) (P.root a)) \\cdot P.coroot i \\in \\operatorname{range}(P.Polarization.domRestrict (P.rootSpan R))$$$
Lean4
theorem four_smul_rootForm_sq_eq_coxeterWeight_smul (i j : ι) :
4 • (P.RootForm (P.root i) (P.root j)) ^ 2 =
P.coxeterWeight i j • (P.RootForm (P.root i) (P.root i) * P.RootForm (P.root j) (P.root j)) :=
by
have hij : 4 • (P.RootForm (P.root i)) (P.root j) = 2 • P.toLinearMap (P.root j) (2 • P.Polarization (P.root i)) := by
rw [← toLinearMap_apply_apply_Polarization, LinearMap.map_smul_of_tower, ← smul_assoc, Nat.nsmul_eq_mul]
have hji : 2 • (P.RootForm (P.root i)) (P.root j) = P.toLinearMap (P.root i) (2 • P.Polarization (P.root j)) := by
rw [show (P.RootForm (P.root i)) (P.root j) = (P.RootForm (P.root j)) (P.root i) by apply (rootForm_symmetric P).eq,
← toLinearMap_apply_apply_Polarization, LinearMap.map_smul_of_tower]
rw [sq, nsmul_eq_mul, ← mul_assoc, ← nsmul_eq_mul, hij, ← rootForm_self_smul_coroot, smul_mul_assoc 2, ←
mul_smul_comm, hji, ← rootForm_self_smul_coroot, map_smul, ← pairing, map_smul, ← pairing, smul_eq_mul, smul_eq_mul,
smul_eq_mul, coxeterWeight]
ring
