add_apply — Mathlib

English

If D1 and D2 are derivations R → M over A, then their sum D1 + D2 is again a derivation, and for every a ∈ A we have (D1 + D2)(a) = D1(a) + D2(a).

Русский

Если D1 и D2 — деривации R → M над A, то их сумма D1 + D2 также является деривацией, и для каждого a ∈ A имеет место (D1 + D2)(a) = D1(a) + D2(a).

LaTeX

$$$\forall D_1 D_2 : \mathrm{Derivation}(R,A,M)\; (\forall a : A),\ (D_1 + D_2)(a) = D_1(a) + D_2(a).$$$

Lean4

theorem add_apply : (D1 + D2) a = D1 a + D2 a :=
  rfl

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