Commit 2023-12-07 06:32 0b3cbe39

View on Github →

feat: Lemmas for pointwise smul on submodules. (#8654)

Estimated changes

Modified Mathlib/Algebra/Algebra/Operations.lean

added theorem Submodule.mem_smul_iff_inv_mul_mem

added theorem Submodule.mul_mem_smul_iff

added theorem Submodule.span_singleton_mul