English
There exists a well-defined scalar action of the quotient ring R/I on M, given by (b + I) · x = b · x for all b ∈ R and x ∈ M, because I annihilates M on the IsTorsionBySet assumption.
Русский
Существует корректное скалярное действие кольца R/I на M, заданное (b + I) · x = b · x, поскольку элементы I аннулируют M при условии IsTorsionBySet.
LaTeX
$$$(\\exists\, \\text{smul})\\; :\\; (R/I) \\times M \\to M\\quad\\text{such that}\\quad (b+I)\\cdot x = b\\cdot x\\quad\\text{for all } b\\in R, x\\in M.$$$
Lean4
/-- can't be an instance because `hM` can't be inferred -/
def hasSMul (hM : IsTorsionBySet R M I) : SMul (R ⧸ I) M where
smul
b := QuotientAddGroup.lift I.toAddSubgroup (smulAddHom R M) (by rwa [isTorsionBySet_iff_subset_annihilator] at hM) b
