mathlib3

74457cb0 - feat(data/polynomial,field_theory): `(minpoly A x).map f ≠ 1` (#9451)

feat(data/polynomial,field_theory): `(minpoly A x).map f ≠ 1` (#9451) We use this result to generalize `minpoly.not_is_unit` from integral domains to nontrivial `comm_ring`s. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>