single_smul — Mathlib

English

Let R be a commutative ring, M an R-module. For any i ∈ N, r ∈ R, m ∈ M, the polynomial-module element obtained by multiplying the i-th singleton by r·m equals r times the i-th singleton of m: single R i (r · m) = r · single R i m.

Русский

Пусть R — коммутативное кольцо, M — R-модуль. Для любого i ∈ ℕ, r ∈ R и m ∈ M выполняется: single R i (r · m) = r · single R i m.

LaTeX

$$$single_R i (r \cdot m) = r \cdot single_R i m$$$

Lean4

theorem single_smul (i : ℕ) (r : R) (m : M) : single R i (r • m) = r • single R i m :=
  (lsingle R i).map_smul r m

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