Theorem Submodule.mul_mem_smul_iff

Modification history

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