prod_nat_mod — Mathlib

English

For a finite set s and f: ι → ℕ, the product modulo n distributes over the residues: (∏_{i∈s} f(i)) mod n = (∏_{i∈s} (f(i) mod n)) mod n.

Русский

Для конечного множества s и f: ι → ℕ произведение по модулю n равно произведению остатков: (∏ f(i)) mod n = ∏ (f(i) mod n) mod n.

LaTeX

$$$$\left(\prod_{i \in s} f(i)\right) \\% n = \left(\prod_{i \in s} (f(i) \\% n)\right) \\% n.$$$$

Lean4

theorem prod_nat_mod (s : Finset ι) (n : ℕ) (f : ι → ℕ) : (∏ i ∈ s, f i) % n = (∏ i ∈ s, f i % n) % n :=
  (Multiset.prod_nat_mod _ _).trans <| by rw [Finset.prod, Multiset.map_map]; rfl

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