mathlib

7d864755 - feat(data/polynomial): eq_one_of_is_unit_of_monic (#2823)