isPrime_of_isPrime_prod_top' — Mathlib

English

For any prime I ⊆ R, the ideal I × ⊤ is prime in R × S.

Русский

Для любого простого I в R, I × ⊤ простый в R × S.

LaTeX

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

Lean4

theorem isPrime_of_isPrime_prod_top' {I : Ideal S} (h : (Ideal.prod (⊤ : Ideal R) I).IsPrime) : I.IsPrime :=
  by
  apply isPrime_of_isPrime_prod_top (S := R)
  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 := R) (S := S))

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