compQuadraticMap_polarBilin — Mathlib

English

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

Русский

Для Q и f полярBilin (Q.comp f) равно вытягиванию polarBilin Q по f по обеим координатам.

LaTeX

$$$ polarBilin (Q.comp f) = polarBilin Q .compr₂ f f $$$

Lean4

theorem _root_.LinearMap.compQuadraticMap_polarBilin (f : N →ₗ[R] N') (Q : QuadraticMap R M N) :
    (f.compQuadraticMap' Q).polarBilin = Q.polarBilin.compr₂ f :=
  by
  ext
  rw [polarBilin_apply_apply, compr₂_apply, polarBilin_apply_apply, LinearMap.compQuadraticMap_polar]

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