Theorem Submodule.setSemiring_smul_def

Modification history

2026-10-13 18:29
Mathlib/Algebra/Algebra/Operations.lean
refactor: review of `SetSemiring` (#37603) …
Modified Submodule.setSemiring_smul_defView on Github →
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 →