sum_div — Mathlib

English

Let s be a multiset of natural numbers and R a AddCommMonoid with one. The cast of the sum of s equals the sum of the casts: (↑s.sum : R) = (s.map (↑)).sum.

Русский

Пусть s — мультимножество натуральных чисел, R — аддитивная моноида с единицей. Образ суммы s равен сумме образов: (↑s.sum : R) = (s.map (↑)).sum.

LaTeX

$$$\left(\uparrow s.sum\right) = \sum (\uparrow)\, s$$$

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 := eq_or_ne n 0
  · simp
  rw [Int.ediv_eq_iff_eq_mul_left hn (dvd_sum hf), sum_mul]
  refine sum_congr rfl fun s hs ↦ ?_
  rw [Int.ediv_mul_cancel (hf _ hs)]

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