mathlib

83490903 - feat(ring_theory/polynomial/cyclotomic): generalize some lemmas to `[ring R]` (#17555)

feat(ring_theory/polynomial/cyclotomic): generalize some lemmas to `[ring R]` (#17555) * Generalize some lemmas from commutative (semi)rings to (semi)rings. * Use `finset.erase s 1` instead of `s \ {1}`.