seq_add — Mathlib

English

Applying f to a sum equals the sum of applying f to each addend: f <*> (x + y) = (f <*> x) + (f <*> y).

Русский

Применение f к сумме равно сумме применений: f <*> (x + y) = (f <*> x) + (f <*> y).

LaTeX

$$$ \forall {\alpha \beta} (f : FreeAbelianGroup(\alpha \to \beta)) (x y : FreeAbelianGroup(\alpha)),\; f <*> (x + y) = (f <*> x) + (f <*> y)$$$

Lean4

@[simp]
theorem seq_add (f : FreeAbelianGroup (α → β)) (x y : FreeAbelianGroup α) : f <*> x + y = (f <*> x) + (f <*> y) :=
  (seqAddGroupHom f).map_add x y

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