English
For odd a,b: J(a|b) = qrSign(b,a) · J(b|a).
Русский
Для нечётных a, b выполняется: J(a|b) = qrSign(b,a) · J(b|a).
LaTeX
$$$\forall a,b \in \mathbb{N},\ Pa n \text{Odd}(a) \land \text{Odd}(b) \implies J(a|b) = qrSign(b,a) \cdot J(b|a)$$$
Lean4
/-- The **Law of Quadratic Reciprocity for the Jacobi symbol**, version with `qrSign` -/
theorem quadratic_reciprocity' {a b : ℕ} (ha : Odd a) (hb : Odd b) : J(a | b) = qrSign b a * J(b | a) := by
-- define the right-hand side for fixed `a` as a `ℕ →* ℤ`
let rhs : ℕ → ℕ →* ℤ := fun a =>
{ toFun := fun x => qrSign x a * J(x | a)
map_one' := by convert ← mul_one (M := ℤ) _; (on_goal 1 => symm); all_goals apply one_left
map_mul' := fun x y => by simp_rw [qrSign.mul_left x y a, Nat.cast_mul, mul_left, mul_mul_mul_comm] }
have rhs_apply : ∀ a b : ℕ, rhs a b = qrSign b a * J(b | a) := fun a b => rfl
refine value_at a (rhs a) (fun p pp hp => Eq.symm ?_) hb
have hpo := pp.eq_two_or_odd'.resolve_left hp
rw [@legendreSym.to_jacobiSym p ⟨pp⟩, rhs_apply, Nat.cast_id, qrSign.eq_iff_eq hpo ha, qrSign.symm hpo ha]
refine value_at p (rhs p) (fun q pq hq => ?_) ha
have hqo := pq.eq_two_or_odd'.resolve_left hq
rw [rhs_apply, Nat.cast_id, ← @legendreSym.to_jacobiSym p ⟨pp⟩, qrSign.symm hqo hpo, qrSign.neg_one_pow hpo hqo,
@legendreSym.quadratic_reciprocity' p q ⟨pp⟩ ⟨pq⟩ hp hq]
