mk_smul — Mathlib

English

If I is two-sided and hM is IsTorsionBySet, then for any b ∈ R and x ∈ M, the action of the coset b + I on x matches the original scalar action: (b + I) • x = b • x.

Русский

Если I двусторонний и hM есть IsTorsionBySet, то для любого b ∈ R и x ∈ M действие косета b + I на x совпадает с исходным действием: (b + I) • x = b • x.

LaTeX

$$$[I.IsTwoSided]~(hM:IsTorsionBySet R M I)\\;\\Rightarrow\\; (Ideal.Quotient.mk I\\ b) \\cdot x = b \\cdot x.$$

Lean4

@[simp]
theorem mk_smul [I.IsTwoSided] (hM : IsTorsionBySet R M I) (b : R) (x : M) :
    haveI := hM.hasSMul
    Ideal.Quotient.mk I b • x = b • x :=
  rfl

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