d_mul — Mathlib

English

For a derivation D: B → M over a ring A with B a ring, the differential D satisfies D(b b') = b · D(b') + b' · D(b) for all b,b' in B.

Русский

Для деривации D: B → M над кольцом A, если B — кольцо, то выполняется D(b b') = b D(b') + b' D(b) для всех b,b' ∈ B.

LaTeX

$$$\\forall b,b' \\in B:\\; D.d(b \\cdot b') = b \\cdot D.d(b') + b' \\cdot D.d(b).$$$

Lean4

@[simp]
theorem d_mul (b b' : B) : D.d (b * b') = b • D.d b' + b' • D.d b := by simp [d]

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