English
Composing a quadratic map with a right linear map yields a new quadratic map: (Q : N→P)∘f with (f: M→N) defines Q(f(x)).
Русский
Композит квадратичной карты с линейным отображением справа образует новую квадратичную карту: (Q ∘ f)(x) = Q(f(x)).
LaTeX
$$$ (Q : QuadraticMap\\,R\\,N\\,P) \\circ f\\; (x) = Q(f(x)) $ for all x, where $f: M \\to N$ is linear.$$
Lean4
/-- Compose the quadratic map with a linear function on the right. -/
def comp (Q : QuadraticMap R N P) (f : M →ₗ[R] N) : QuadraticMap R M P
where
toFun x := Q (f x)
toFun_smul a x := by simp only [Q.map_smul, map_smul]
exists_companion' :=
let ⟨B, h⟩ := Q.exists_companion
⟨B.compl₁₂ f f, fun x y => by simp_rw [f.map_add]; exact h (f x) (f y)⟩
