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)
:
A variant of SModEq.smul, where the scalar belongs to an ideal.