Commit 2021-10-01 10:38 74457cb0

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_rings.