Theorem Submodule.restrictScalars_mul

Modification history

2024-11-08 15:45
Mathlib/Algebra/Algebra/Operations.lean
refactor: generalize Mul of Submodule and SMul of Ideal on Submodule to noncommutative setting (#17708) …
Modified Submodule.restrictScalars_mulView on Github →
2023-11-27 17:05
Mathlib/Algebra/Algebra/Operations.lean
feat: Add `Submodule.restrictScalars_mul`. (#8649)
Added Submodule.restrictScalars_mulView on Github →