polarBilin_comp — Mathlib

English

For Q and f, polarBilin (Q.comp f) equals the pullback of polarBilin Q by f in both arguments.

Русский

Для Q и линейного отображения f полярная билинейная карта (Q.comp f) равна отталкиванию полярной билинейной карты Q по f в обоих аргументах.

LaTeX

$$$ polarBilin (Q.comp f) = LinearMap.compl₁₂ (polarBilin Q) f f $$$

Lean4

theorem _root_.QuadraticMap.polarBilin_comp (Q : QuadraticMap R N' N) (f : M →ₗ[R] N') :
    polarBilin (Q.comp f) = LinearMap.compl₁₂ (polarBilin Q) f f :=
  LinearMap.ext₂ <| fun x y => by simp [polar]

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