Theorems · Definition · field theory

Polynomial.nthRootsFinset

ℕ → {R : Type u_1} → R → [inst : CommRing R] → [IsDomain R] → Finset R

The multiset nthRoots ↑n a as a Finset. Previously nthRootsFinset n was defined to be nthRoots n (1 : R) as a Finset. That situation can be recovered by setting a to be (1 : R)

Defined in

Mathlib.Algebra.Polynomial.Roots

Cited by

23 results in Mathlib

Foundations

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

Assumes

CommRingIsDomain