mathlib

bef50a4d - feat(field_theory/minpoly): Minimal polynomials of degree one (#5844)

feat(field_theory/minpoly): Minimal polynomials of degree one (#5844) If the minimal polynomial has degree one then the element in question lies in the base ring. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>