Mathlib v3 is deprecated. Go to Mathlib v4

Theorem adjoin_root.minpoly.to_adjoin.injective

Modification history

2023-01-06 22:53
src/ring_theory/adjoin_root.lean
chore({ring_theory, field_theory}/*): fix imports to make #18021 less messy (#18065) …
Deleted adjoin_root.minpoly.to_adjoin.injectiveView on Github →
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.injectiveView on Github →