Facts about the gaussian integers relying on quadratic reciprocity.

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

theorem GaussianInt.mod_four_eq_three_of_nat_prime_of_prime (p : ℕ) [hp : Fact (Nat.Prime p)] (hpi : Prime ↑p) : p % 4 = 3

theorem GaussianInt.prime_of_nat_prime_of_mod_four_eq_three (p : ℕ) [hp : Fact (Nat.Prime p)] (hp3 : p % 4 = 3) : Prime ↑p

theorem GaussianInt.prime_iff_mod_four_eq_three_of_nat_prime (p : ℕ) [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