Theorem Submodule.mem_smul_iff_inv_mul_mem

Modification history

2025-04-08 22:12
Mathlib/Algebra/Algebra/Operations.lean
feat: generalize Mathlib.Algebra.Algebra + Module (#23190) …
Modified Submodule.mem_smul_iff_inv_mul_memView on Github →
2023-12-07 06:32
Mathlib/Algebra/Algebra/Operations.lean
feat: Lemmas for pointwise smul on submodules. (#8654)
Added Submodule.mem_smul_iff_inv_mul_memView on Github →