mathlib3
f4bce070 - chore(ring_theory): split `ring_theory.algebra_tower` (#17480)

Commit
3 years ago
chore(ring_theory): split `ring_theory.algebra_tower` (#17480) Remove the dependency of the file `ring_theory.algebra_tower` on `ring_theory.adjoin.fg` by moving all those results to a new file `ring_theory.adjoin.tower`, because that dependency carries with it a large amount of imports from `mv_polynomial`. In a follow-up PR I want to adjust `ring_theory.finiteness` so we don't need to import `mv_polynomial` there either, with the eventual goal that our definition of finite dimensional vector space doesn't import `mv_polynomial`.
Author
Parents
Loading