Theorems · Theorem · field theory

Polynomial.isRoot_map_iff

∀ {S : Type v} [inst : CommSemiring S] {R : Type u_1} [inst_1 : CommRing R] {f : R →+* S} {x : R} {p : Polynomial R},
  Function.Injective ⇑f → ((Polynomial.map f p).IsRoot (f x) ↔ p.IsRoot x)

Defined in

Mathlib.Algebra.Polynomial.Eval.Coeff

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommRing