Commit 2026-05-22 09:11 f466e8ce

View on Github →

feat(Algebra/Module/Submodule/Ker): restricting a linear map to its kernel (#39658) We add the lemma saying that restricting a linear map to its kernel yields the zero map. In passing, we generalise a couple of results from linear to semilinear maps.

Estimated changes