Theorem LinearMap.range_domRestrict

Modification history

2026-07-01 17:54
Mathlib/Algebra/Module/Submodule/Range.lean
chore: cleanup API around LinearMap.surjective_domRestrict_iff (#41235) …
Modified LinearMap.range_domRestrictView on Github →
2024-10-17 16:19
Mathlib/Algebra/Module/Submodule/Range.lean
feat(Algebra/Module/Submodule): lemmas about `domRestrict` (#17806) …
Added LinearMap.range_domRestrictView on Github →