associated_pi — Mathlib

English

The polar bilinear form of the pi-map equals the sum of the polar bilinear forms of each component evaluated pointwise.

Русский

Полярная билинеарная форма карты pi равна сумме полярных билинейных форм по компонентам, вычисленных по точкам.

LaTeX

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

Lean4

@[simp]
theorem associated_pi [Invertible (2 : R)] (Q : ∀ i, QuadraticMap R (Mᵢ i) P) :
    associated (pi Q) = ∑ i, (Q i).associated.compl₁₂ (.proj i) (.proj i) :=
  by
  dsimp [associated, associatedHom]
  rw [polarBilin_pi, Finset.smul_sum]
  rfl

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