sum_mapDomain_index — Mathlib

English

Sum after a mapDomain is equal to a sum over the original object with h applied to the mapped argument.

Русский

Сумма после mapDomain равна сумме по исходному объекту с применением h к преобразованному аргументу.

LaTeX

$$$$ sum (mapDomain f v) h = sum v (\\lambda a m, h (f a) m) $$$$

Lean4

theorem sum_mapDomain_index {k' : Type*} [AddCommMonoid k'] {h : G' → k → k'} (h_zero : ∀ (b : G'), h b 0 = 0)
    (h_add : ∀ (b : G') (m₁ m₂ : k), h b (m₁ + m₂) = h b m₁ + h b m₂) :
    sum (mapDomain f v) h = sum v fun a m ↦ h (f a) m :=
  (sum_sum_index h_zero h_add).trans <| sum_congr fun _ _ ↦ sum_single_index (h_zero _)

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