compQuadraticMap_polar — Mathlib

English

A variation of polar composition showing how polar interacts with a linear map under quadratic maps.

Русский

Вариация совместимости полярирования с линейным отображением в рамках квадратичных отображений.

LaTeX

$$$ polar (f.compQuadraticMap' Q) x y = f (polar Q x y) $$$

Lean4

theorem _root_.LinearMap.compQuadraticMap_polar [CommSemiring S] [Algebra S R] [Module S N] [Module S N']
    [IsScalarTower S R N] [Module S M] [IsScalarTower S R M] (f : N →ₗ[S] N') (Q : QuadraticMap R M N) (x y : M) :
    polar (f.compQuadraticMap' Q) x y = f (polar Q x y) := by simp [polar]

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