Theorem Submodule.map_smul_le_map

Modification history

2026-05-25 15:44
Mathlib/Algebra/Module/Submodule/Map.lean
feat: LinearMap.HasFiniteRange and the associated relation (#39468) …
Added Submodule.map_smul_le_mapView on Github →