mathlib

a480160a - feat(data/polynomial): generalize theorems from nonzero_comm_ring to comm_ring (#653)