mk_smul — Mathlib

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

Похожие утверждения