mathlib3

bdf3e970 - chore(data/polynomial/laurent): remove unused case distinction (#14490)