English
There is a scalar action of any monoid S on QuadraticMap R M N, defined by (a • Q)(x) = a • Q(x), making QuadraticMap into an S-module compatible with evaluation.
Русский
Существует действие скаляра со стороны любого моноида S на квадратичное отображение Q: (a • Q)(x) = a • Q(x); таким образом квадратичное отображение образует модуль над S, совместимый с вычислением значения.
LaTeX
$$$ (a\\,\\cdot\\, Q)(x) = a\\,\\cdot\\, Q(x) $$$
Lean4
/-- `QuadraticMap R M N` inherits the scalar action from any algebra over `R`.
This provides an `R`-action via `Algebra.id`. -/
instance : SMul S (QuadraticMap R M N) :=
⟨fun a Q =>
{ toFun := a • ⇑Q
toFun_smul := fun b x => by rw [Pi.smul_apply, Q.map_smul, Pi.smul_apply, smul_comm]
exists_companion' :=
let ⟨B, h⟩ := Q.exists_companion
letI := SMulCommClass.symm S R N
⟨a • B, by simp [h]⟩ }⟩
