isPrime_ideal_prod_top' — Mathlib

English

If I × J is prime, then either I = ⊤ or J = ⊤.

Русский

Если I × J прост, то либо I = ⊤, либо J = ⊤.

LaTeX

$$$(I \\mathrm{prod} J) \\text{ IsPrime} \\Rightarrow (I=\\top) \\lor (J=\\top)$$$

Lean4

theorem isPrime_ideal_prod_top' {I : Ideal S} [h : I.IsPrime] : (prod (⊤ : Ideal R) I).IsPrime :=
  by
  letI : IsPrime (prod I (⊤ : Ideal R)) := isPrime_ideal_prod_top
  rw [← map_prodComm_prod]
    -- Note: couldn't synthesize the right instances without the `R` and `S` hints

  exact map_isPrime_of_equiv (RingEquiv.prodComm (R := S) (S := R))

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