mathlib

d89bfc41 - feat(field_theory/minpoly): remove `is_integral` requirement from `unique'` (#7064)

feat(field_theory/minpoly): remove `is_integral` requirement from `unique'` (#7064) `unique'` had an extraneous requirement on `is_integral`, which could be inferred from the other arguments. This is a small step towards #5258, but is a breaking change; `unique'` now needs one less argument, which will break all current code using `unique'`.