Theorem LinearMap.range_domRestrict_le_range

Modification history

2024-04-26 19:07
Mathlib/Algebra/Module/Submodule/Range.lean
chore: move LinearMap.range into its own file (#12378)
Modified LinearMap.range_domRestrict_le_rangeView on Github →
2023-10-02 15:34
Mathlib/LinearAlgebra/Basic.lean
feat: disintegration of Lebesgue measure in vector spaces (#7252) …
Added LinearMap.range_domRestrict_le_rangeView on Github →