Theorems · Definition · field theory

Polynomial.aroots

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

Given a polynomial p with coefficients in a ring T and a T-algebra S, aroots p S is the multiset of roots of p regarded as a polynomial over S.

Defined in

Mathlib.Algebra.Polynomial.Roots

Cited by

89 results in Mathlib

Foundations

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

Assumes

CommRingCommRingIsDomainAlgebra