Theorem LinearMap.submoduleImage_apply_of_le

Modification history

2025-04-08 22:12
Mathlib/Algebra/Module/Submodule/Range.lean
feat: generalize Mathlib.Algebra.Algebra + Module (#23190) …
Modified LinearMap.submoduleImage_apply_of_leView on Github →
2024-04-26 19:07
Mathlib/Algebra/Module/Submodule/Range.lean
chore: move LinearMap.range into its own file (#12378)
Modified LinearMap.submoduleImage_apply_of_leView on Github →
2023-11-17 19:26
Mathlib/LinearAlgebra/Basic.lean
refactor: rename `Submodule.ofLe` to `Submodule.inclusion` (#8470) …
Added LinearMap.submoduleImage_apply_of_leView on Github →