Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-15 16:09 a35ddf20

View on Github →

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.

Estimated changes