prod_int_mod — Mathlib

English

Modulo n, the product of integers respects residues modulo n: prod(s) mod n equals prod of residues modulo n.

Русский

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

LaTeX

$$$( \\mathrm{prod} \\; s ) \\bmod n = \\big( (s.map (\\\\lambda x. x \\bmod n)) .prod \\big) \\bmod n$$$

Lean4

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

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