evalAddMonoidHom — Mathlib

English

There is a canonical AddMonoidHom from QuadraticMap R M N to M → N, given by Q ↦ (x ↦ Q(x)).

Русский

Существует канонический AddMonoidHom: квадратичная карта отображается в функцию x ↦ Q(x).

LaTeX

$$$\\text{coeFnAddMonoidHom} : \\ QuadraticMap(R,M,N) \\to_{+} (M \\to N)$ with $\\big(\\text{coeFnAddMonoidHom}(Q)\\big)(x) = Q(x)$.$$

Lean4

/-- Evaluation on a particular element of the module `M` is an additive map on quadratic maps. -/
@[simps! apply]
def evalAddMonoidHom (m : M) : QuadraticMap R M N →+ N :=
  (Pi.evalAddMonoidHom _ m).comp coeFnAddMonoidHom

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