list_prod_left — Mathlib

English

For any l : List ℤ and n : ℕ, J(l.prod | n) = (l.map (a ↦ J(a | n))).prod.

Русский

Для любого списка l : List ℤ и n : ℕ выполняется J(l.prod | n) = ∏_{a ∈ l} J(a | n).

LaTeX

$$$ J(l.prod | n) = (l.map (\\lambda a. J(a | n))).prod $$$

Lean4

/-- We can pull out a product over a list in the first argument of the Jacobi symbol. -/
theorem list_prod_left {l : List ℤ} {n : ℕ} : J(l.prod | n) = (l.map fun a => J(a | n)).prod := by
  induction l with
  | nil => simp only [List.prod_nil, List.map_nil, one_left]
  | cons n l' ih => rw [List.map, List.prod_cons, List.prod_cons, mul_left, ih]

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