Theorems · Theorem · commutative algebra

IsLocalRing.isUnit_aeval_derivative_minpoly_of_adjoin_eq_top

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsLocalRing S]
  [IsLocalRing R] [Module.Finite R S] [FaithfulSMul R S] [Algebra.Etale R S] {β : S},
  R[β] = ⊤ → IsUnit ((Polynomial.aeval β) (Polynomial.derivative (minpoly R β)))

If R → S is étale and R[β] = S, then f'(β) is a unit in S, where f = minpoly R β. The proof reduces to separability of the residue field extension via minpoly_map_residue.

Defined in

Mathlib.RingTheory.LocalRing.Etale

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsLocalRingIsLocalRingModule.FiniteFaithfulSMulAlgebra.Etale