quadratic_reciprocity_one_mod_four

English

If p ≡ q ≡ 3 mod 4 and p ≠ 2, q ≠ 2, then (q/p) = (p/q).

Русский

Если p ≡ q ≡ 3 mod 4 и p ≠ 2, q ≠ 2, тогда (q/p) = (p/q).

LaTeX

$$$ p \equiv q \equiv 3 \\pmod{4} \\Rightarrow \\left( \\frac{q}{p} \\right) = \\left( \\frac{p}{q} \\right).$$$

Lean4

/-- The Law of Quadratic Reciprocity: if `p` and `q` are odd primes and `p % 4 = 1`,
then `(q / p) = (p / q)`. -/
theorem quadratic_reciprocity_one_mod_four (hp : p % 4 = 1) (hq : q ≠ 2) : legendreSym q p = legendreSym p q := by
  rw [quadratic_reciprocity' ((Prime.mod_two_eq_one_iff_ne_two Fact.out).mp (odd_of_mod_four_eq_one hp)) hq, pow_mul,
    neg_one_pow_div_two_of_one_mod_four hp, one_pow, one_mul]

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