ideal_prod_prime_aux — Mathlib

English

Prime ideals in a product R × S are exactly those of the form p × S or R × p, where p is prime in R or S.

Русский

Простые идеалы в произведении R × S имеют вид p × S или R × p, где p прост в R или S.

LaTeX

$$$I.IsPrime \\iff (\\exists p \\ IsPrime p.R \\land I = p.prod \\top) \\lor (\\exists p \\ IsPrime p.S \\land I = \\top.prod p)$$

Lean4

theorem ideal_prod_prime_aux {I : Ideal R} {J : Ideal S} : (Ideal.prod I J).IsPrime → I = ⊤ ∨ J = ⊤ :=
  by
  contrapose!
  simp only [ne_top_iff_one, isPrime_iff, not_and, not_forall, not_or]
  exact fun ⟨hI, hJ⟩ _ => ⟨⟨0, 1⟩, ⟨1, 0⟩, by simp, by simp [hJ], by simp [hI]⟩

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