polarBilin_pi — Mathlib

English

The associated map of the pi is the sum of the associated maps of each component, projected appropriately.

Русский

Ассоциированная карта пи равна сумме ассоциированных карт компонент, корректно проецируемых.

LaTeX

$$$ \\mathrm{associated}(\\pi Q) = \\sum_i \\mathrm{associated}(Q_i) \\circ_{12} (\\mathrm{proj}_i, \\mathrm{proj}_i). $$$

Lean4

@[simp]
theorem polarBilin_pi (Q : ∀ i, QuadraticMap R (Mᵢ i) P) :
    (pi Q).polarBilin = ∑ i, (Q i).polarBilin.compl₁₂ (.proj i) (.proj i) :=
  LinearMap.ext₂ fun x y => (polar_pi _ _ _).trans <| by simp

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