mul_right' — Mathlib

English

J(a|b1*b2) = J(a|b1) J(a|b2) provided b1,b2 ≠ 0.

Русский

При b1,b2 ≠ 0 выполняется J(a|b1 b2) = J(a|b1) J(a|b2).

LaTeX

$$$J(a|b_1 b_2) = J(a|b_1) \cdot J(a|b_2)$, при $b_1,b_2 \neq 0$$$

Lean4

/-- The Jacobi symbol is multiplicative in its second argument. -/
theorem mul_right' (a : ℤ) {b₁ b₂ : ℕ} (hb₁ : b₁ ≠ 0) (hb₂ : b₂ ≠ 0) : J(a | b₁ * b₂) = J(a | b₁) * J(a | b₂) :=
  by
  rw [jacobiSym, ((perm_primeFactorsList_mul hb₁ hb₂).pmap _).prod_eq, List.pmap_append, List.prod_append]
  pick_goal 2
  · exact fun p hp => (List.mem_append.mp hp).elim prime_of_mem_primeFactorsList prime_of_mem_primeFactorsList
  · rfl

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