Commit 2026-03-10 02:02 a182019b
View on Github →feat(Algebra): add two lemmas about submodule smul (#35646)
This is the first PR split from the larger PR #34936 to make the review process easier.
It adds the following two lemmas regarding pointwise smul and restrictScalars:
Submodule.restrictScalars_image_smul_eq and Submodule.restrictScalars_map_smul_eq