Commit 2025-04-23 03:41 5e32622d

View on Github →

refactor(Algebra/Polynomial/Roots): nthRoots as a Finset (#23293) If nthRoots n a is defined as the roots of (X : R[X]) ^ n - C a as a multiset then surely nthRootsFinset n a should be the roots of (X : R[X]) ^ n - C a as a Finset?

Estimated changes

Modified Mathlib/Algebra/Polynomial/Roots.lean

added theorem Polynomial.map_mem_nthRootsFinset_one

modified theorem Polynomial.mem_nthRootsFinset

modified theorem Polynomial.ne_zero_of_mem_nthRootsFinset

modified def Polynomial.nthRootsFinset

modified theorem Polynomial.nthRootsFinset_def

modified theorem Polynomial.nthRootsFinset_zero

modified theorem Polynomial.one_mem_nthRootsFinset

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean

Modified Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean