mathlib3 documentation

number_theory.zsqrtd.quadratic_reciprocity

Facts about the gaussian integers relying on quadratic reciprocity. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main statements #

prime_iff_mod_four_eq_three_of_nat_prime A prime natural number is prime in ℤ[i] if and only if it is 3 mod 4

source
theorem gaussian_int.mod_four_eq_three_of_nat_prime_of_prime (p : ℕ) [hp : fact (nat.prime p)] (hpi : prime ↑p) :
p % 4 = 3
source
theorem gaussian_int.prime_of_nat_prime_of_mod_four_eq_three (p : ℕ) [hp : fact (nat.prime p)] (hp3 : p % 4 = 3) :
prime ↑p
source
theorem gaussian_int.prime_iff_mod_four_eq_three_of_nat_prime (p : ℕ) [hp : fact (nat.prime p)] :
prime ↑p ↔ p % 4 = 3

A prime natural number is prime in ℤ[i] if and only if it is 3 mod 4