mathlib

a35ddf20 - chore(algebra/algebra): reduce imports for `algebra.algebra.tower` (#17476)

chore(algebra/algebra): reduce imports for `algebra.algebra.tower` (#17476) This splits `algebra.algebra.tower` into two files: `algebra.algebra.tower.basic` and `algebra.algebra.subalgebra.tower`. The motivation behind this PR is that `algebra.algebra.tower` is a relatively fundamental and popular file to import (especially since it used to contain `is_scalar_tower`), but its import tree also includes relatively complicated files such as `ring_theory.ideal.operations`. By splitting off these less popular dependencies we can save quite a bit of complexity in the import graph. Co-authored-by: Vierkantor <vierkantor@vierkantor.com>