Theorems · Theorem · field theory

Polynomial.preimage_eval_singleton

∀ {R : Type u} {a : R} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R},
  p ≠ Polynomial.C a → (fun x => Polynomial.eval x p) ⁻¹' {a} = (p - Polynomial.C a).rootSet R

Defined in

Mathlib.Algebra.Polynomial.Roots

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDomain