map_single — Mathlib

English

The map R' f sends a singleton to the singleton of the mapped element: map R' f (single R i m) = single R' i (f m).

Русский

Преобразование map R' f переводит одинокий элемент в одинокий элемент: map R' f (single R i m) = single R' i (f m).

LaTeX

$$map R' f (single R i m) = single R' i (f m)$$

Lean4

@[simp]
theorem map_single (f : M →ₗ[R] M') (i : ℕ) (m : M) : map R' f (single R i m) = single R' i (f m) :=
  Finsupp.mapRange_single (hf := f.map_zero)

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