prod_nat_mod — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem prod_nat_mod (l : List ℕ) (n : ℕ) : l.prod % n = (l.map (· % n)).prod % n := by
  induction l with
  | nil => simp only [map_nil]
  | cons a l ih => simpa only [prod_cons, map_cons, Nat.mod_mul_mod, Nat.mul_mod_mod] using congr((a * $ih) % n)

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