Theorem Submodule.smul_def

Modification history

2024-11-20 11:42

Mathlib/Algebra/Algebra/Operations.lean

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

Modified Submodule.smul_def View on Github →

2023-03-04 17:16

Mathlib/Algebra/Algebra/Operations.lean

feat: port Algebra.Algebra.Operations (#2568) …

Added Submodule.smul_def View on Github →