Theorems · Definition · field theory

Polynomial.rootSet

{T : Type w} →
  [inst : CommRing T] → Polynomial T → (S : Type u_1) → [inst_1 : CommRing S] → [IsDomain S] → [Algebra T S] → Set S

The set of distinct roots of p in S. If you have a non-separable polynomial, use Polynomial.aroots for the multiset where multiple roots have the appropriate multiplicity.

Defined in

Mathlib.Algebra.Polynomial.Roots

Cited by

101 results in Mathlib

Foundations

Depth 131 from the axioms, rests on 3,042 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingIsDomainAlgebra