single_sub — Mathlib

English

For AddGroup, single i (x − y) = single i x − single i y.

Русский

Для группы сложения единичная функция на разность: single i (x − y) = single i x − single i y.

LaTeX

$$$ \\mathrm{single}_i (x - y) = \\mathrm{single}_i x - \\mathrm{single}_i y $$$

Lean4

@[simp]
theorem single_sub {β : ι → Type v} [∀ i, AddGroup (β i)] (i : ι) (x y : β i) :
    single i (x - y) = single i x - single i y :=
  (singleAddHom β i).map_sub x y

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