English
If x is killed by the derivative on B (i.e., x′ = 0) under the differential structure containing constants, then x comes from A via the algebra map, i.e., x lies in the image of A under algebraMap A B.
Русский
Если элемент x фиксирован производной в B (x′ = 0) в условиях дифференциальной структуры, содержащей константы, то x получается из A через алгебраическую карту, то есть x лежит в образе A в B.
LaTeX
$$$\exists a\in A:\quad \iota(a) = x$, equivalently $x \in \mathrm{im}(\iota)$, given $x' = 0$ in $B$.$$
Lean4
theorem mem_range_of_deriv_eq_zero (A : Type*) {B : Type*} [CommRing A] [CommRing B] [Algebra A B] [Differential B]
[Differential.ContainConstants A B] {x : B} (h : x′ = 0) : x ∈ (algebraMap A B).range :=
Differential.ContainConstants.mem_range_of_deriv_eq_zero h
