Commit 2023-08-11 13:05 cf872fff

chore: protect Submodule.map_smul (#6521) In the current situation, open Submodule prevents using the (exported) lemma SMulHomClass.map_smul without qualifying it explicitly, which is a bit of a shame since we need it all the time for linear maps. This also means that using map_smul for Submodule.map_smul will never work outside of namespace Submodule, so we might as well make it protected.