instAddCommMonoid — Mathlib

English

The set of derivations Derivation(R,A,M) forms an additive commutative monoid under pointwise addition with the zero derivation, i.e., (D1 + D2)(a) = D1(a) + D2(a) and 0(a) = 0.

Русский

Множество дериваций Derivation(R,A,M) образует аддитивный коммутативный моноид: (D1 + D2)(a) = D1(a) + D2(a), 0(a) = 0.

LaTeX

$$$(D_1 + D_2)(a) = D_1(a) + D_2(a), \quad 0(a) = 0 \quad(\forall a \in A).$$$

Lean4

instance : AddCommMonoid (Derivation R A M) :=
  coe_injective.addCommMonoid _ coe_zero coe_add fun _ _ => rfl

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