Commit 2024-11-20 11:42 7600042b

View on Github →

feat: IsScalarTower and SMulCommClass instances for pointwise actions of submodules (#19214) Moves:

Submodule.smul_def → Submodule.setSemiring_smul_def From GrowthInGroups

Estimated changes

Modified Mathlib/Algebra/Algebra/Operations.lean

added theorem Submodule.mul_def

added theorem Submodule.setSemiring_smul_def

deleted theorem Submodule.smul_def

Modified Mathlib/Algebra/Module/Submodule/Pointwise.lean

added theorem Submodule.smul_def