theory Algebra_Towers imports Compatible_Scalar_Actions begin section ‹Scalar towers› text ‹ The locale \<^locale>‹algebra_tower› packages three existing module actions and the single additional compatibility law required by a tower. The remaining theories derive functorial, basis, dimension, trace, and norm interfaces from it. › end