Commit 2024-05-22 06:25 29980c83

View on Github →

Feat(Algebra/Module/Submodule/Pointwise): Generalize set_smul_eq_iSup as in TODO (#13103) Generalize set_smul_eq_iSup so it works with actions on R-submodules of bimodules.

Estimated changes

modified theorem Submodule.set_smul_eq_iSup