Theorems · Theorem · commutative algebra

Differential.algHom_deriv

∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Differential A] {R : Type u_2} [inst_2 : CommRing R]
  [inst_3 : Differential R] [inst_4 : Algebra A R] [DifferentialAlgebra A R] {R' : Type u_3} [inst_6 : CommRing R']
  [inst_7 : Differential R'] [inst_8 : Algebra A R'] [DifferentialAlgebra A R'] [IsDomain R'] [Nontrivial R]
  (f : R →ₐ[A] R'), Function.Injective ⇑f → ∀ (x : R), IsSeparable A x → f x′ = (f x)′

Defined in

Mathlib.RingTheory.Derivation.MapCoeffs

Cited by

2 results in Mathlib

Foundations

Depth 120 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingDifferentialCommRingDifferentialAlgebraDifferentialAlgebraCommRingDifferentialAlgebraDifferentialAlgebraIsDomainNontrivial