quadratic_reciprocity_three_mod_four

English

For odd a,b, the reciprocity law is governed by the parity of a mod 4 and b mod 4: if both are 3 mod 4, J(a|b) = - J(b|a); otherwise J(a|b) = J(b|a).

Русский

Для нечётных a,b закон взаимности зависит от остатка mod 4: если оба ≡ 3 mod 4, тогда J(a|b) = - J(b|a); иначе J(a|b) = J(b|a).

LaTeX

$$$\forall a,b \in \mathbb{N},\ \bigl( (a \bmod 4 = 3) \land (b \bmod 4 = 3) \bigr) \Rightarrow J(a|b) = - J(b|a) \text{and appropriate otherwise}$$$

Lean4

/-- The Law of Quadratic Reciprocity for the Jacobi symbol: if `a` and `b` are natural numbers
both congruent to `3` mod `4`, then `J(a | b) = -J(b | a)`. -/
theorem quadratic_reciprocity_three_mod_four {a b : ℕ} (ha : a % 4 = 3) (hb : b % 4 = 3) : J(a | b) = -J(b | a) :=
  by
  let nop := @neg_one_pow_div_two_of_three_mod_four
  rw [quadratic_reciprocity, pow_mul, nop ha, nop hb, neg_one_mul] <;> rwa [odd_iff, odd_of_mod_four_eq_three]

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