Commit 2023-12-03 14:46 3e423640

View on Github →

feat: add some lemmas about nthRootsFinset (#7464) From flt-regular.

Estimated changes

Modified Mathlib/Data/Polynomial/RingDivision.lean

added theorem Polynomial.mul_mem_nthRootsFinset

added theorem Polynomial.ne_zero_of_mem_nthRootsFinset

added theorem Polynomial.one_mem_nthRootsFinset