Pointwise lemmas for modular equivalence

In this file, we record more lemmas about SModEq on elements of modules or rings.

theorem SModEq.smul' {R : Type u_1} [Ring R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] {U : Submodule R M} {x y : M} (hxy : x ≡ y [SMOD U]) {c : R} (hc : c ∈ I) : c • x ≡ c • y [SMOD I • U]

A variant of SModEq.smul, where the scalar belongs to an ideal.