Theorem Submodule.set_smul_mono_right

Modification history

2025-01-06 10:15
Mathlib/Algebra/Module/Submodule/Pointwise.lean
chore: remove >9 month old deprecations (#20505)
Deleted Submodule.set_smul_mono_rightView on Github →
2024-05-26 06:15
Mathlib/Algebra/Module/Submodule/Pointwise.lean
chore(Algebra): add missing deprecation dates (#12598)
Modified Submodule.set_smul_mono_rightView on Github →
2024-04-02 23:42
Mathlib/Algebra/Module/Submodule/Pointwise.lean
feat: pointwise scalar multiplication is monotone (#11809) …
Modified Submodule.set_smul_mono_rightView on Github →
2023-12-27 05:26
Mathlib/Algebra/Module/Submodule/Pointwise.lean
feat: In a ring, sets act on submodules (#7140) …
Added Submodule.set_smul_mono_rightView on Github →