Theorem minpoly.unique'
Modification history
2023-01-14 21:04
src/field_theory/minpoly/basic.lean
feat(ring_theory/power_basis): minpoly_gen is always the minimal polynomial (#18117) …
Added minpoly.unique'View on Github →2021-10-19 20:59
src/field_theory/minpoly.lean
refactor(*): rename some declarations ending with '' (#9504)
Deleted minpoly.unique'View on Github →2021-04-07 10:30
src/field_theory/minpoly.lean
feat(field_theory/minpoly): remove `is_integral` requirement from `unique'` (#7064) …
Modified minpoly.unique'View on Github →2021-01-18 23:02
src/field_theory/minpoly.lean
refactor(field_theory|ring_theory|linear_algebra): minpoly A x (#5774) …
Modified minpoly.unique'View on Github →