English
In the separable setting, for f: R →ₐ[A] R' injective, and x ∈ R with IsSeparable A x, we have f(x′) = (f x)′. This is a variant of the previous statement under weaker hypotheses.
Русский
В разделимом случае, если f: R →ₐ[A] R' инъективно, и x ∈ R удовлетворяет IsSeparable A x, то выполняется f(x′) = (f x)′. Это вариант предыдущего утверждения.
LaTeX
$$$\forall \{A : Type\*\} [\mathrm{CommRing} A] [\mathrm{Differential } A] {R : Type\*} [\mathrm{CommRing} R] [\mathrm{Differential } R] [Algebra A R] {R' : Type\*} [\mathrm{CommRing} R'] [\mathrm{Differential } R'] [Algebra A R'] [IsDomain R'] (f : R \toₐ[A] R') (hf : Function.Injective f) (x : R), IsSeparable A x → f(x′) = (f x)′$$
Lean4
theorem algEquiv_deriv (f : R ≃ₐ[A] R') (x : R) (h : IsSeparable A x) : f (x′) = (f x)′ :=
haveI := f.nontrivial
algHom_deriv f.toAlgHom f.injective x h
