instSub — Mathlib

English

There is a Sub instance on Derivation: D1 - D2 defines a derivation with Leibniz property De(a b) = a b, etc.

Русский

Существует операция вычитания на Derivation: D1 - D2 задаёт новый вывод с линейной и лейбницовой свойствами.

LaTeX

$$Derivation.instSub : Sub (Derivation R A M)$$

Lean4

instance : Sub (Derivation R A M) :=
  ⟨fun D1 D2 =>
    mk' (D1 - D2 : A →ₗ[R] M) fun a b => by
      simp only [LinearMap.sub_apply, leibniz, coeFn_coe, smul_sub, add_sub_add_comm]⟩

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