val_sum — Mathlib

English

A variant of linearity of valuation under finite sums, stated with simp attributes: the same as Val Sum but tagged for simplification.

Русский

Вариант линейности валюации под конечные суммы, помеченный как упрощение.

LaTeX

$$$ \\forall \\iota, (s:\\mathrm{Finset}\\, \\iota) , \\forall f:\\iota \\to \\mathrm{AdicCompletion}(I,M), \\sum_i (f_i).val = (\\sum_i f_i).val $$$

Lean4

@[simp, norm_cast]
theorem val_sum {ι : Type*} (s : Finset ι) (f : ι → AdicCompletion I M) : (∑ i ∈ s, f i).val = ∑ i ∈ s, (f i).val := by
  simp_rw [← funext (incl_apply _ _ _), map_sum]

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