coeFnAddMonoidHom — Mathlib

English

There is an AddCommMonoid structure on Derivation(R,A,M) compatible with the pointwise addition, giving a canonical additive group structure.

Русский

Существует структура AddCommMonoid на Derivation(R,A,M), согласующаяся с пофункциональным сложением по точкам, задающая каноническую аддитивную структуру.

LaTeX

$$$\mathrm{Derivation}(R,A,M)$ is an AddCommMonoid with $(D_1 + D_2)(a) = D_1(a) + D_2(a)$.$$

Lean4

/-- `coeFn` as an `AddMonoidHom`. -/
def coeFnAddMonoidHom : Derivation R A M →+ A → M where
  toFun := (⇑)
  map_zero' := coe_zero
  map_add' := coe_add

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