embDomain_add — Mathlib

English

The embDomain map preserves addition in FinSupp: applying embDomain to a sum equals the sum of embDomains.

Русский

Функция embDomain сохраняет сложение в FinSupp: применение embDomain к сумме равно сумме embDomain.

LaTeX

$$$\operatorname{embDomain} f (v + w) = \operatorname{embDomain} f\, v + \operatorname{embDomain} f\, w$$$

Lean4

@[simp]
theorem embDomain_add (f : ι ↪ F) (v w : ι →₀ M) : embDomain f (v + w) = embDomain f v + embDomain f w :=
  (embDomain.addMonoidHom f).map_add v w

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