mathlib3

0a6c26ee - feat(ring_theory/power_basis): minpoly_gen is always the minimal polynomial (#18117)

feat(ring_theory/power_basis): minpoly_gen is always the minimal polynomial (#18117) + add `minpoly.unique'`, a characterization for being the minimal polynomial. + golf various proofs and remove some unnecessary typeclass assumptions.