sum_nat_mod — Mathlib

English

Modulo n, the sum of a list equals the sum of each element modulo n, modulo n again.

Русский

По модулю n сумма списка равна сумме каждого элемента по модулю n, взятой по модулю n повторно.

LaTeX

$$$\sum l \bmod n = (\sum (l.map (\\cdot \\mod n))).\\mod n$$$

Lean4

theorem sum_nat_mod (l : List ℕ) (n : ℕ) : l.sum % n = (l.map (· % n)).sum % n := by
  induction l with
  | nil => simp only [map_nil]
  | cons a l ih => simpa only [map_cons, sum_cons, Nat.mod_add_mod, Nat.add_mod_mod] using congr((a + $ih) % n)

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