Theorem LinearMap.injective_restrict_iff

Modification history

2026-07-02 16:39
Mathlib/Algebra/Module/Submodule/Ker.lean
chore: cleanup API around LinearMap.injective_domRestrict_iff (#41229) …
Added LinearMap.injective_restrict_iffView on Github →