sum_int_mod — Mathlib

English

For a finite set s and f: ι → ℤ, the sum modulo an integer n distributes over residues: (∑ f(i)) mod n = (∑ (f(i) mod n)) mod n.

Русский

Для конечного множества s и f: ι → ℤ сумма по модулю n распадается на сумму остатков: (∑ f(i)) mod n = ∑ (f(i) mod n) mod n.

LaTeX

$$$$\left(\sum_{i \in s} f(i)\right) \% n = \left(\sum_{i \in s} (f(i) \% n)\right) \% n.$$$$

Lean4

theorem sum_int_mod (s : Finset ι) (n : ℤ) (f : ι → ℤ) : (∑ i ∈ s, f i) % n = (∑ i ∈ s, f i % n) % n :=
  (Multiset.sum_int_mod _ _).trans <| by rw [Finset.sum, Multiset.map_map]; rfl

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