Commit 2021-04-07 10:30 d89bfc41
View on Github →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'.