Commit 2023-01-06 22:53 3e00d81b

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'