English
Let Q be a quadratic map from M to N over R, and let f be a left-linear map N →ₗ[S] P with appropriate scalar-tower compatibility. Then the map x ↦ f(Q x) is a quadratic map from M to P over S.
Русский
Пусть Q — квадратичное отображение из M в N над R, и пусть f — линейное отображение слева N →ₗ[S] P с надлежащей совместимостью торов скаляров. Тогда отображение x ↦ f(Q x) образует квадратичное отображение из M в P над S.
LaTeX
$$$\exists Q' : \text{QuadraticMap } S M P, \forall x \in M, Q'(x) = f(Q(x)).$$$
Lean4
/-- Compose a quadratic map with a linear function on the left. -/
@[simps! +simpRhs]
def _root_.LinearMap.compQuadraticMap' [CommSemiring S] [Algebra S R] [Module S N] [Module S M] [IsScalarTower S R N]
[IsScalarTower S R M] [Module S P] (f : N →ₗ[S] P) (Q : QuadraticMap R M N) : QuadraticMap S M P :=
_root_.LinearMap.compQuadraticMap f Q.restrictScalars
