prime_iff_mod_four_eq_three_of_nat_prime

English

A natural prime p is Gaussian-prime in ℤ[i] if and only if p ≡ 3 mod 4.

Русский

Натуральное простое число p является гауссовым простым в ℤ[i] тогда и только тогда, когда p ≡ 3 (mod 4).

LaTeX

$$$ \text{Prime}(p) \leftrightarrow p \equiv 3 \pmod{4} $$$

Lean4

/-- A prime natural number is prime in `ℤ[i]` if and only if it is `3` mod `4` -/
theorem prime_iff_mod_four_eq_three_of_nat_prime (p : ℕ) [Fact p.Prime] : Prime (p : ℤ[i]) ↔ p % 4 = 3 :=
  ⟨mod_four_eq_three_of_nat_prime_of_prime p, prime_of_nat_prime_of_mod_four_eq_three p⟩

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