Theorems · Theorem · commutative algebra

IsLocalRing.eq_of_eval_eq_zero_of_not_isUnit_sub

∀ {R : Type u_1} [inst : CommRing R] [IsLocalRing R] {f : Polynomial R} {a b : R},
  Polynomial.eval a f = 0 →
    Polynomial.eval b f = 0 → ¬IsUnit (a - b) → IsUnit (Polynomial.eval a (Polynomial.derivative f)) → a = b

[Stacks Tag 06RR](https://stacks.math.columbia.edu/tag/06RR)

Defined in

Mathlib.RingTheory.Henselian

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsLocalRing