Theorem Submodule.smul_def

Modification history

2026-04-15 08:14
Mathlib/Algebra/Module/Submodule/Pointwise.lean
chore(LinearAlgebra/Span): reverse import order between Submodule/Pointwise and Span/Basic (#38013) …
Modified Submodule.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) …
Modified Submodule.smul_defView on Github →
2023-03-04 17:16
Mathlib/Algebra/Algebra/Operations.lean
feat: port Algebra.Algebra.Operations (#2568) …
Added Submodule.smul_defView on Github →