Theorem Submodule.restrictScalars_map_smul_eq

Modification history

2026-03-10 02:02
Mathlib/RingTheory/Ideal/Maps.lean
feat(Algebra): add two lemmas about submodule smul (#35646) …
Added Submodule.restrictScalars_map_smul_eqView on Github →