Mathlib v3 is deprecated. Go to Mathlib v4

Def algebra.adjoin.power_basis'

Modification history

2023-01-27 01:10
src/field_theory/minpoly/is_integrally_closed.lean
chore(ring_theory): protect `algebra.is_integral` (#18178)
Modified algebra.adjoin.power_basis'View on Github →
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) …
Modified algebra.adjoin.power_basis'View 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 algebra.adjoin.power_basis'View on Github →