prod_int_mod — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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