Mathlib v3 is deprecated. Go to Mathlib v4

Theorem adjoin_root.minpoly.to_adjoin.surjective

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_adjoin.surjectiveView on Github →