Theorem Submodule.toAddSubmonoid_restrictScalars

Modification history

2024-01-15 21:28
Mathlib/Algebra/Module/Submodule/RestrictScalars.lean
chore: gather results about `Submodule.restrictScalars` into new file (#9765) …
Added Submodule.toAddSubmonoid_restrictScalarsView on Github →