Theorem Submodule.setSemiring_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) …
Added Submodule.setSemiring_smul_defView on Github →