quadratic_reciprocity_one_mod_four'

English

If a ≡ 3 mod 4 and b ≡ 3 mod 4, then J(a|b) = - J(b|a).

Русский

Если a ≡ 3 mod 4 и b ≡ 3 mod 4, то J(a|b) = - J(b|a).

LaTeX

$$$\forall a,b \in \mathbb{N},\ a \equiv 3 \pmod{4} \land b \equiv 3 \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` odd and `b % 4 = 1`, then `J(a | b) = J(b | a)`. -/
theorem quadratic_reciprocity_one_mod_four' {a b : ℕ} (ha : Odd a) (hb : b % 4 = 1) : J(a | b) = J(b | a) :=
  (quadratic_reciprocity_one_mod_four hb ha).symm

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