sum_int_mod — Mathlib

English

Modulo n, the sum of integers behaves compatibly with taking residues modulo n: sum(s) mod n equals sum of residues modulo n.

Русский

По модулю n сумма целых чисел ведет себя согласованно с остатками по модулю n: сумма по модулю n равна сумме остатков по модулю n.

LaTeX

$$$s.sum \\bmod n = \\big( (s.map (\\\\lambda x. x \\bmod n)) .sum \\big) \\bmod n$$$

Lean4

theorem sum_int_mod (s : Multiset ℤ) (n : ℤ) : s.sum % n = (s.map (· % n)).sum % n := by
  induction s using Multiset.induction <;> simp [Int.add_emod, *]

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