sum_div — Mathlib

English

For a list of natural numbers s, the natural cast of the sum equals the sum of the casts of the elements, i.e., (sum s).cast = sum (map cast s).

Русский

Для списка натуральных чисел s верно, что приведенное к R суммирование равно сумме приведений элементов: (sum s).cast = (sum (map cast s)).

LaTeX

$$$\\left(\\sum_{i} s_i\\right)^{\\text{cast}} = \\sum_{i} (s_i^{\\text{cast}})$$$

Lean4

protected theorem sum_div (hf : ∀ i ∈ s, n ∣ f i) : (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n :=
  by
  obtain rfl | hn := n.eq_zero_or_pos
  · simp
  rw [Nat.div_eq_iff_eq_mul_left hn (dvd_sum hf), sum_mul]
  refine sum_congr rfl fun s hs ↦ ?_
  rw [Nat.div_mul_cancel (hf _ hs)]

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