English
Let A and B be commutative rings with an algebra structure A → B and differential structures that make B a differential A-algebra. Then for every a in A, the derivative of a computed in A, when viewed in B via the algebra map, equals the derivative of its image in B.
Русский
Пусть A и B — коммутативные кольца, между ними задана структура алгебры A → B и имеются дифференциальные структуры, делающие B дифференциальной A-алгеброй. Тогда для каждого элемента a ∈ A производная a, взятая в A, равна производной образа a в B по алгебраической карте.
LaTeX
$$$\displaystyle \text{Let } \iota: A \to B \text{ be the algebra map. Then for all } a \in A:\quad D_B(\iota(a)) = \iota(D_A(a)).$$$
Lean4
@[norm_cast]
theorem coe_deriv {A : Type*} {B : Type*} [CommRing A] [CommRing B] [Algebra A B] [Differential A] [Differential B]
[DifferentialAlgebra A B] (a : A) : (a′ : A) = (a : B)′ :=
(DifferentialAlgebra.deriv_algebraMap _).symm
