quadratic_reciprocity_one_mod_four

English

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

Русский

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

LaTeX

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

Lean4

/-- The Law of Quadratic Reciprocity for the Jacobi symbol: if `a` and `b` are natural numbers
with `a % 4 = 1` and `b` odd, then `J(a | b) = J(b | a)`. -/
theorem quadratic_reciprocity_one_mod_four {a b : ℕ} (ha : a % 4 = 1) (hb : Odd b) : J(a | b) = J(b | a) := by
  rw [quadratic_reciprocity (odd_iff.mpr (odd_of_mod_four_eq_one ha)) hb, pow_mul,
    neg_one_pow_div_two_of_one_mod_four ha, one_pow, one_mul]

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