Commit 2022-11-12 05:40 f4bce070

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.