instAdd — Mathlib

English

The coercion respects addition: (D1 + D2) corresponds to the sum of their linear maps.

Русский

Коэрция уважает сумму: (D1 + D2) соответствует сумме их линейных отображений.

LaTeX

$$$\uparrow(D1 + D2) = D1 + D2$ as linear maps.$$

Lean4

instance : Add (Derivation R A M) :=
  ⟨fun D1 D2 =>
    { toLinearMap := D1 + D2
      map_one_eq_zero' := by simp
      leibniz' := fun a b => by simp only [leibniz, LinearMap.add_apply, coeFn_coe, smul_add, add_add_add_comm] }⟩

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