instSMulSubtypeMemTorsion' — Mathlib

English

There is a natural scalar action of S on the torsion' R M S, defined by lifting representatives in M and using smul in M.

Русский

Существует естественное скалярное действие S на torsion' R M S, задаваемое по представителям в M через умножение в M.

LaTeX

$$SMul S (torsion' R M S).$$

Lean4

@[simps]
instance : SMul S (torsion' R M S) :=
  ⟨fun s x =>
    ⟨s • (x : M), by
      obtain ⟨x, a, h⟩ := x
      use a
      dsimp
      rw [smul_comm, h, smul_zero]⟩⟩

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