Commit 2026-01-29 15:56 b621b1dd
View on Github →chore(Algebra): move LinearMap.ker_restrictScalars (#33788)
Resolve an old TODO by moving LinearMap.ker_restrictScalars to a location in Mathlib/Algebra/Module/Submodule.
The TODO referenced lemmas in plural, but only LinearMap.ker_restrictScalars seemed to fit. I assume any other lemmas might already have been moved at an earlier point.