Theorems · Theorem · field theory

Polynomial.bUnion_roots_finite

∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : DecidableEq S]
  (m : R →+* S) (d : ℕ) {U : Set R},
  U.Finite → (⋃ f, ⋃ (_ : f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U), ↑(Polynomial.map m f).roots.toFinset).Finite

The set of roots of all polynomials of bounded degree and having coefficients in a finite set is finite.

Defined in

Mathlib.Algebra.Polynomial.Roots

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemiringCommRingIsDomainDecidableEq