Mathlib v3 is deprecated. Go to Mathlib v4

Def adjoin_root.minpoly.to_adjoin

Modification history

2022-07-18 15:26
src/ring_theory/adjoin_root.lean
feat(ring_theory/adjoin_root): add lemmas for GCD domains (#14981) …
Added adjoin_root.minpoly.to_adjoinView on Github →