quadratic_reciprocity — Mathlib

English

If a ≡ 1 mod 4 and b is odd, then J(a|b) = J(b|a).

Русский

Если a ≡ 1 mod 4 и b нечётно, то J(a|b) = J(b|a).

LaTeX

$$$\forall a,b \in \mathbb{N},\ a \equiv 1 \pmod{4} \; \text{and} \; \text{Odd}(b) \implies J(a|b) = J(b|a)$$$

Lean4

/-- The Law of Quadratic Reciprocity for the Jacobi symbol -/
theorem quadratic_reciprocity {a b : ℕ} (ha : Odd a) (hb : Odd b) : J(a | b) = (-1) ^ (a / 2 * (b / 2)) * J(b | a) := by
  rw [← qrSign.neg_one_pow ha hb, qrSign.symm ha hb, quadratic_reciprocity' ha hb]

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