sum_nat_mod — Mathlib

English

For a finite set s and f: ι → ℕ, the sum modulo n distributes over the sum of residues: (∑_{i∈s} f(i)) mod n = (∑_{i∈s} (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_nat_mod (s : Finset ι) (n : ℕ) (f : ι → ℕ) : (∑ i ∈ s, f i) % n = (∑ i ∈ s, f i % n) % n :=
  (Multiset.sum_nat_mod _ _).trans <| by rw [Finset.sum, Multiset.map_map]; rfl

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