Theorems · Theorem · field theory

Polynomial.mem_roots_map_of_injective

∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : Semiring S] {p : Polynomial S}
  {f : S →+* R},
  Function.Injective ⇑f → ∀ {x : R}, p ≠ 0 → (x ∈ (Polynomial.map f p).roots ↔ Polynomial.eval₂ f x p = 0)

Defined in

Mathlib.Algebra.Polynomial.Roots

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainSemiring