Def alg_equiv.adjoin_singleton_equiv_adjoin_root_minimal_polynomial

Modification history

2021-01-17 00:33
src/field_theory/splitting_field.lean
chore(field_theory|ring_theory|linear_algebra): rename minimal_polynomial to minpoly (#5771) …
Deleted alg_equiv.adjoin_singleton_equiv_adjoin_root_minimal_polynomialView on Github →
2020-08-06 16:42
src/field_theory/splitting_field.lean
feat(field_theory/splitting_field): splitting field unique (#3654) …
Added alg_equiv.adjoin_singleton_equiv_adjoin_root_minimal_polynomialView on Github →