mathlib3

71985dc5 - feat(field_theory/minpoly): generalize statements about GCD domains (#14979)

feat(field_theory/minpoly): generalize statements about GCD domains (#14979) Currently, the statements about the minimal polynomial over a GCD domain `R` require the element to be in a `K`-algebra, where `K` is the fraction field of `R`. We remove this assumption. From flt-regular.