val_sum_apply — Mathlib

English

For any finite index set, and any n, the valuation commutes with summation pointwise: (sum_i f_i).val(n) = sum_i f_i.val(n).

Русский

Для конечного множества индексов и фиксированного n валюация берёт сумму по i координат: (sum_i f_i).val(n) = sum_i f_i.val(n).

LaTeX

$$$ \\forall s, \\forall f:s \\to \\mathrm{AdicCompletion}(I,M), (s.sum (\\lambda i, f(i))).val(n) = s.sum (\\lambda i, (f(i).val(n))) $$$

Lean4

theorem val_sum_apply {ι : Type*} (s : Finset ι) (f : ι → AdicCompletion I M) (n : ℕ) :
    (∑ i ∈ s, f i).val n = ∑ i ∈ s, (f i).val n := by simp

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