corootForm_self_smul_root — Mathlib

English

The four-fold smul of the composition CoPolarization ∘ Polarization evaluated at a root equals a product of RootForm and CorootForm acting on the root, scaled by root.

Русский

Четыре раза поляризация ∘ поляризация применяется к корню и даёт произведение RootForm и CorootForm, умноженное на корень.

LaTeX

$$$(4 \\cdot P.CoPolarization \\circ P.Polarization)(P.root i) = (P.RootForm(P.root i)(P.root i) * P.CorootForm(P.coroot i)(P.coroot i)) \\cdot P.root i$$$

Lean4

theorem corootForm_self_smul_root (i : ι) :
    (P.CorootForm (P.coroot i) (P.coroot i)) • P.root i = 2 • P.CoPolarization (P.coroot i) :=
  rootForm_self_smul_coroot (P.flip) i

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