Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-06 22:53 3e00d81b

View on Github →

chore({ring_theory, field_theory}/*): fix imports to make #18021 less messy (#18065) PR #18021 makes some changes to the theory of minpoly, which has the net effect that the structure of imports has to be changed for some files. This is a bit painful so I've decided to open a new PR instead of doing it in #18021. This PR also moves the following definitions from ring_theory/adjoin_root.lean to field_theory/minpoly/gcd_monoid.lean:

  • minpoly.to_adjoin.injective
  • minpoly.equiv_adjoin
  • algebra.adjoin.power_basis'
  • power_basis.of_gen_mem_adjoin'

Estimated changes