English
If span {r} is two-sided, then for hM IsTorsionBy R M r, we have (Ideal.span{r})-quotient action satisfies (Ideal.Quotient.mk (span { r })) b · x = b · x.
Русский
Если span{r} образует двустороннюю идеал и hM IsTorsionBy R M r, то действие косета по Ideal.Quotient.mk (span{r}) на x совпадает с обычным умножением на b.
LaTeX
$$$[ (\\operatorname{span}\\{r\\}).IsTwoSided ] (hM:IsTorsionBy R M r) \\Rightarrow\\; (Ideal.Quotient.mk (Ideal.span { r })\\, b) \\cdot x = b \\cdot x.$$
Lean4
@[simp]
theorem mk_smul [(Ideal.span { r }).IsTwoSided] (hM : IsTorsionBy R M r) (b : R) (x : M) :
haveI := hM.hasSMul
Ideal.Quotient.mk (Ideal.span { r }) b • x = b • x :=
rfl