mathlib

77003ce2 - refactor(field_theory|ring_theory|linear_algebra): minpoly A x (#5774)

refactor(field_theory|ring_theory|linear_algebra): minpoly A x (#5774) This PR refactors the definition of `minpoly` to ``` noncomputable def minpoly (x : B) : polynomial A := if hx : is_integral A x then well_founded.min degree_lt_wf _ hx else 0 ``` The benefit is that we can write `minpoly A x` instead of `minpoly hx` for `hx : is_integral A x`. The resulting code is more readable, and some lemmas are true without the `hx` assumption.