coeFnAddMonoidHom — Mathlib

English

The evaluation at a fixed m ∈ M gives an AddMonoidHom from QuadraticMap R M N to N by Q ↦ Q(m).

Русский

Оценка в фиксированном элементе m даёт гомоморфизм AddMonoid из QuadraticMap R M N в N, Q ↦ Q(m).

LaTeX

$$$\\text{evalAddMonoidHom}(m) : \\ QuadraticMap(R,M,N) \\to_{+} N$, $\\big[ \\text{ev}_m(Q) = Q(m) \\big]$ and $\\text{ev}_m(Q_1+Q_2) = \\text{ev}_m(Q_1) + \\text{ev}_m(Q_2)$.$$

Lean4

/-- `@CoeFn (QuadraticMap R M)` as an `AddMonoidHom`.

This API mirrors `AddMonoidHom.coeFn`. -/
@[simps apply]
def coeFnAddMonoidHom : QuadraticMap R M N →+ M → N
    where
  toFun := DFunLike.coe
  map_zero' := coeFn_zero
  map_add' := coeFn_add

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