English
If D: A → M is an R-linear map satisfying the Leibniz rule D(ab) = a·D(b) + b·D(a), then D defines a derivation Derivation R A M.
Русский
Пусть D: A → M линейно по R и удовлетворяет правилу Лейбница D(ab) = a·D(b) + b·D(a). Тогда D определяет вывод Derivation R A M.
LaTeX
$$$\text{If } D: A \to M\text{ is } R\text{-linear and } D(ab) = a \cdot D(b) + b \cdot D(a)\text{ for all } a,b\in A,\; \text{then } D\in \operatorname{Derivation} R A M.$$$
Lean4
/-- Define `Derivation R A M` from a linear map when `M` is cancellative by verifying the Leibniz
rule. -/
def mk' (D : A →ₗ[R] M) (h : ∀ a b, D (a * b) = a • D b + b • D a) : Derivation R A M
where
toLinearMap := D
map_one_eq_zero' := (add_eq_left (a := D 1)).1 <| by simpa only [one_smul, one_mul] using (h 1 1).symm
leibniz' := h
