Commit 2024-10-23 12:15 e98856ac

refactor: redefine Module.annihilator using RingHom.ker (#18094) The original definition LinearMap.ker (LinearMap.lsmul R M) doesn't work in the noncommutative setting, because lsmul isn't R-linear if R is noncommutative, and also LinearMap.ker isn't obviously a two-sided ideal. We also move Module.annihilator from Ideal/Operations to Ideal/Maps (where RingHom.ker is defined).