toSpanSingleton_add — Mathlib

English

The span singleton map is additive: toSpanSingleton(x+y) = toSpanSingleton(x) + toSpanSingleton(y).

Русский

Спан-одиночка является аддитивной: toSpanSingleton(х+у) = toSpanSingleton(х) + toSpanSingleton(у).

LaTeX

$$$toSpanSingleton\,R\,M\ (x+y) = toSpanSingleton\,R\,M\ x + toSpanSingleton\,R\,M\ y$$$

Lean4

theorem toSpanSingleton_add (x y : M) : toSpanSingleton R M (x + y) = toSpanSingleton R M x + toSpanSingleton R M y :=
  by ext; simp

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