English
We can pull out a product in the second argument: J(a | l.prod) = ∏_{n ∈ l} J(a | n) for hl : ∀ n ∈ l, n ≠ 0.
Русский
Можно вынести произведение во втором аргументе: J(a | l.prod) = ∏_{n ∈ l} J(a | n) при условии hl : ∀ n ∈ l, n ≠ 0.
LaTeX
$$$ J(a | l.prod) = \prod_{n \in l} J(a | n) $$$
Lean4
/-- We can pull out a product over a list in the second argument of the Jacobi symbol. -/
theorem list_prod_right {a : ℤ} {l : List ℕ} (hl : ∀ n ∈ l, n ≠ 0) : J(a | l.prod) = (l.map fun n => J(a | n)).prod :=
by
induction l with
| nil => simp only [List.prod_nil, one_right, List.map_nil]
| cons n l' ih =>
have hn := hl n List.mem_cons_self
have hl' := List.prod_ne_zero fun hf => hl 0 (List.mem_cons_of_mem _ hf) rfl
have h := fun m hm =>
hl m
(List.mem_cons_of_mem _ hm)
-- `∀ (m : ℕ), m ∈ l' → m ≠ 0`
rw [List.map, List.prod_cons, List.prod_cons, mul_right' a hn hl', ih h]
