mkDerivation_apply — Mathlib

English

There is a uniqueness principle for derivations on polynomial rings based on their action on X and their behavior on sums.

Русский

Существуют принципы уникальности для дериваций на кольцах полиномов, основанные на действии на X и на сложении.

LaTeX

$$$D_1 X = D_2 X \Rightarrow D_1 = D_2$$$

Lean4

theorem mkDerivation_apply (a : A) (f : R[X]) : mkDerivation R a f = derivative f • a := by rfl

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