Theorem Submodule.restrictScalars_image_smul_eq

Modification history

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