mkLinearMap — Mathlib

English

The map sending m to m/1, i.e., m ↦ mk(m,1), is an R-linear map M → LocalizedModule S M.

Русский

Отображение m ↦ m/1, то есть m ↦ mk(m,1), является R-образом линейного отображения M → LocalizedModule S M.

LaTeX

$$$\\text{mkLinearMap}: M \\to_{R} \\mathrm{LocalizedModule}(S,M),\\quad m \\mapsto \\mathrm{mk}(m,1).$$$

Lean4

/-- The function `m ↦ m / 1` as an `R`-linear map.
-/
@[simps]
noncomputable def mkLinearMap : M →ₗ[R] LocalizedModule S M
    where
  toFun m := mk m 1
  map_add' x y := by simp [mk_add_mk]
  map_smul' _ _ := (smul'_mk _ _ _).symm

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