quadratic_reciprocity_if — Mathlib

English

The Jacobi symbol J(a|b) depends only on b modulo 4a when b is odd.

Русский

Символ Якоби J(a|b) зависит только от b по модулю 4a, если b нечетно.

LaTeX

$$$\forall a \in \mathbb{N},\forall b \in \mathbb{N},\ \text{Odd}(b) \Rightarrow J(a|b) = J(a|b \bmod (4a))$$$

Lean4

theorem quadratic_reciprocity_if {a b : ℕ} (ha2 : a % 2 = 1) (hb2 : b % 2 = 1) :
    (if a % 4 = 3 ∧ b % 4 = 3 then -J(b | a) else J(b | a)) = J(a | b) :=
  by
  rcases Nat.odd_mod_four_iff.mp ha2 with ha1 | ha3
  · simpa [ha1] using jacobiSym.quadratic_reciprocity_one_mod_four' (Nat.odd_iff.mpr hb2) ha1
  rcases Nat.odd_mod_four_iff.mp hb2 with hb1 | hb3
  · simpa [hb1] using jacobiSym.quadratic_reciprocity_one_mod_four hb1 (Nat.odd_iff.mpr ha2)
  simpa [ha3, hb3] using (jacobiSym.quadratic_reciprocity_three_mod_four ha3 hb3).symm

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