isPrime_of_isPrime_prod_top — Mathlib

English

If I is a prime ideal of R and (I × ⊤) is prime in R × S, then I is prime; similarly for ⊤ × J.

Русский

Если I ⊆ R является простым, и I × ⊤ простый в R × S, тогда I прост; аналогично для ⊤ × J.

LaTeX

$$$(\\mathrm{prod}\\, I \\; (\\top))\\,\\text{IsPrime} \\Rightarrow I\\ \\text{IsPrime}$$$

Lean4

theorem isPrime_of_isPrime_prod_top {I : Ideal R} (h : (Ideal.prod I (⊤ : Ideal S)).IsPrime) : I.IsPrime :=
  by
  constructor
  · contrapose! h
    rw [h, prod_top_top, isPrime_iff]
    simp
  · intro x y hxy
    have : (⟨x, 1⟩ : R × S) * ⟨y, 1⟩ ∈ prod I ⊤ :=
      by
      rw [Prod.mk_mul_mk, mul_one, mem_prod]
      exact ⟨hxy, trivial⟩
    simpa using h.mem_or_mem this

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