map_nsmul — Mathlib

English

For any function f: α → β and n ∈ ℕ, and any multiset s ∈ Multiset α, one has map f (n • s) = n • map f s.

Русский

Для любой функции f: α → β и натурального n выполняется map f (n • s) = n • map f s для любого s ∈ Multiset α.

LaTeX

$$$\operatorname{map} f (n \cdot s) = n \cdot \operatorname{map} f s.$$$

Lean4

theorem map_nsmul (f : α → β) (n : ℕ) (s) : map f (n • s) = n • map f s :=
  (mapAddMonoidHom f).map_nsmul _ _

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