Theorem Submodule.mul_mem_smul_iff

Modification history

2025-10-15 10:28
Mathlib/Algebra/Algebra/Operations.lean
chore(algebra): generalize mul_mem_smul_iff to rings (#30254) …
Modified Submodule.mul_mem_smul_iffView on Github →
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 →