refactor: generalize Mul of Submodule and SMul of Ideal on Submodule to noncommutative setting

[alreadydone]

Instead of using Submodule.map₂ (which doesn't apply in the noncommutative setting), redefine the Mul and SMul to be defeq to AddSubmonoid.mul. In general, if a semiring A is a module over a semiring R such that IsScalarTower R A A is true, then the product of a Submodule R A with a Set A will be a Submodule R A, but we do not need this heterogeneous multiplication yet. We mainly intend to apply this to the case A = R.

Also:

• Change the definition of 1 : Submodule R A from the range of algebraMap R A to the R-span of {1}, which requires fixing many downstream files, but this is the only reasonable definition in the noncommutative setting.

• Generalize some lemmas and SMul to AddSubmonoids

• Redefine (Sub)module.annihilator to work in the noncommutative setting using RingHom.ker; move it from Ideal/Operations to Ideal/Maps (which only imports Ideal/Operations) because RingHom.ker is defined there.

---

Preparation for the Hopkins–Levitzki theorem #17908. E.g. this is necessary to state that the Jacobson radical of an Artinian ring is nilpotent.

• [ ] depends on: #18092
• [x] depends on: #18094
• [x] depends on: #18096