sum_int_mod — Mathlib

English

For integers, the sum modulo n equals the sum of each term modulo n, modulo n.

Русский

Для целых чисел сумма по модулю n равна сумме каждого слагаемого по модулю n, взятому по модулю n.

LaTeX

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

Lean4

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

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