Commit 2024-10-26 13:22 a9b268f6

refactor: change the definition of 1 : Submodule R A to the range of (· • 1) (#18092) Previously, it's defined to be the range of algebraMap R A. In the noncommutative setting, we want to write 1 : Ideal R where Ideal R := Submodule R R, but R isn't an R-algebra if R is not commutative. If we were to introduce a new typeclass by removing the commutes' field from Algebra, we could keep the current definition, but I'd argue that it's still better to use SMul to define 1 : Submodule R A, because Submodule only depends on the Module/SMul, not on the algebraMap/RingHom. Requires fixes in 11 other files.