prime_of_nat_prime_of_mod_four_eq_three

English

If p is a natural prime with p ≡ 3 mod 4, then p remains prime in ℤ[i].

Русский

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

LaTeX

$$Prime (p : \mathbb{Z}[i])$$

Lean4

theorem prime_of_nat_prime_of_mod_four_eq_three (p : ℕ) [Fact p.Prime] (hp3 : p % 4 = 3) : Prime (p : ℤ[i]) :=
  irreducible_iff_prime.1 <|
    by_contradiction fun hpi =>
      let ⟨a, b, hab⟩ := sq_add_sq_of_nat_prime_of_not_irreducible p hpi
      have : ∀ a b : ZMod 4, a ^ 2 + b ^ 2 ≠ (p : ZMod 4) := by rw [← ZMod.natCast_mod p 4, hp3]; decide
      this a b (hab ▸ by simp)

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