Commit 2024-10-17 16:19 c744def5

View on Github →

feat(Algebra/Module/Submodule): lemmas about domRestrict (#17806) From PFR

Estimated changes

Modified Mathlib/Algebra/Module/Submodule/Ker.lean

added theorem LinearMap.ker_domRestrict

Modified Mathlib/Algebra/Module/Submodule/Map.lean

modified theorem Submodule.comap_le_comap_iff_of_surjective

added theorem Submodule.comap_lt_comap_iff_of_surjective

Modified Mathlib/Algebra/Module/Submodule/Range.lean

added theorem LinearMap.range_domRestrict