Mathlib v3 is deprecated. Go to Mathlib v4

Theorem minpoly.to_adjoin.injective

Modification history

2023-01-06 22:53
src/field_theory/minpoly/gcd_monoid.lean
chore({ring_theory, field_theory}/*): fix imports to make #18021 less messy (#18065) …
Added minpoly.to_adjoin.injectiveView on Github →