four_nsmul_coPolarization_compl_polarization_apply_root

English

The square of RootForm between roots i and j, scaled by 4, equals CoxeterWeight(i,j) times the product of root forms at i and j, times 4.

Русский

Квадрат RootForm между корнями i и j, умноженный на 4, равен CoxeterWeight(i,j) умноженному на произведение RootForm(i,i) и RootForm(j,j) и на 4.

LaTeX

$$$$4 \\cdot (P.RootForm(P.root i)(P.root j))^2 = P.coxeterWeight i j \\cdot (P.RootForm(P.root i)(P.root i) \\cdot P.RootForm(P.root j)(P.root j))$$$$

Lean4

theorem four_nsmul_coPolarization_compl_polarization_apply_root (i : ι) :
    (4 • P.CoPolarization ∘ₗ P.Polarization) (P.root i) =
      (P.RootForm (P.root i) (P.root i) * P.CorootForm (P.coroot i) (P.coroot i)) • P.root i :=
  by
  rw [LinearMap.smul_apply, LinearMap.comp_apply, show 4 = 2 * 2 from rfl, mul_smul, ← map_nsmul, ←
    rootForm_self_smul_coroot, map_smul, smul_comm, ← corootForm_self_smul_root, smul_smul]

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