mathlib3

3e00d81b - chore({ring_theory, field_theory}/*): fix imports to make #18021 less messy (#18065)

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' Co-authored-by: Paul Lezeau <paul.lezeau@gmail.com>