Theorem Submodule.span_singleton_mul

Modification history

2023-12-07 06:32
Mathlib/Algebra/Algebra/Operations.lean
feat: Lemmas for pointwise smul on submodules. (#8654)
Added Submodule.span_singleton_mulView on Github →