GaussianInt.prime_iff_mod_four_eq_three_of_nat_prime

theorem GaussianInt.prime_iff_mod_four_eq_three_of_nat_prime : ∀ (p : ℕ) [inst : Fact p.Prime], Prime ↑p ↔ p % 4 = 3

This theorem states that for any prime natural number `p`, `p` is a prime number in the ring of Gaussian integers (`ℤ[i]`) if and only if `p` modulo `4` is equal to `3`. In other words, a natural number `p` retains its primality when considered as a Gaussian integer if it leaves a remainder of `3` when divided by `4`.

More concisely: A natural number `p` is a prime in the ring of Gaussian integers `ℤ[i]` if and only if `p` is congruent to 3 modulo 4.