English
The space of quadratic maps is closed under addition; the sum Q+Q' is a quadratic map with (Q+Q')(x) = Q(x) + Q'(x) and the associated bilinear companion is the sum B + B'.
Русский
Пространство квадратичных отображений замкнуто относительно сложения; сумма Q+Q' является квадратичным отображением, и (Q+Q')(x) = Q(x) + Q'(x); сопряжённое билинейное отображение равно B + B'.
LaTeX
$$$(Q+Q')(x) = Q(x) + Q'(x)$$$
Lean4
instance : Add (QuadraticMap R M N) :=
⟨fun Q Q' =>
{ toFun := Q + Q'
toFun_smul := fun a x => by simp only [Pi.add_apply, smul_add, QuadraticMap.map_smul]
exists_companion' :=
let ⟨B, h⟩ := Q.exists_companion
let ⟨B', h'⟩ := Q'.exists_companion
⟨B + B', fun x y => by simp_rw [Pi.add_apply, h, h', LinearMap.add_apply, add_add_add_comm]⟩ }⟩
