Theorem LinearMap.domRestrict_ker_self

Modification history

2026-05-22 09:11
Mathlib/Algebra/Module/Submodule/Ker.lean
feat(Algebra/Module/Submodule/Ker): restricting a linear map to its kernel (#39658) …
Added LinearMap.domRestrict_ker_selfView on Github →