map_add — Mathlib

English

For any f : α → β and x,y ∈ FreeAbelianGroup α, map f distributes over addition: map f (x+y) = map f x + map f y.

Русский

Для любой f : α → β и элементов x,y ∈ FreeAbelianGroup α отображение через f распределяется по сложению: map f (x+y) = map f x + map f y.

LaTeX

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

Lean4

@[simp]
protected theorem map_add (f : α → β) (x y : FreeAbelianGroup α) : f <$> (x + y) = f <$> x + f <$> y :=
  (lift _).map_add _ _

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