Theorem Submodule.restrictScalars_localized'_smul

Modification history

2025-02-13 08:21
Mathlib/Algebra/Module/LocalizedModule/Submodule.lean
feat(LocalizedModule): expand API (#20340)
Added Submodule.restrictScalars_localized'_smulView on Github →