map_comap_natCastRingHom_int — Mathlib

English

For P : Ideal ℤ, P.IsPrime iff P = ⊥ or ∃ p ∈ ℕ prime with P = span{(p : ℤ)}. Equivalently, prime ideals in ℤ are (0) or generated by a prime integer.

Русский

Для P : Ideal ℤ верно: P IsPrime ⇔ P = ⊥ или ∃ p ∈ ℕ, p Prime и P = span{(p : ℤ)}. Иными словами, простые идеалы ℤ — это (0) или порожденные простым целым числом.

LaTeX

$$$P.IsPrime \iff P = \perp \ \lor\ \exists p \in \mathbb{N}, p.Prime \land P = \mathrm{span}\{(p : \mathbb{Z})\}$$$

Lean4

theorem map_comap_natCastRingHom_int {I : Ideal ℤ} : (I.comap (Nat.castRingHom ℤ)).map (Nat.castRingHom ℤ) = I :=
  map_comap_le.antisymm fun n hn ↦
    n.sign_mul_natAbs ▸ mul_mem_left _ _ <|
      mem_map_of_mem _ (mem_comap.mpr <| show (n.natAbs : ℤ) ∈ I from n.sign_mul_self ▸ mul_mem_left _ _ hn)

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