English
If s and t satisfy the nonemptiness condition, span(s × t) equals prod(span s, span t).
Русский
Если пара множеств удовлетворяет условию непустоты, тогда span(s × t) равно prod(span s, span t).
LaTeX
$$span_prod {s : Set R} {t : Set S} (hst : s.Nonempty ↔ t.Nonempty) : span (Set.instSProd.sprod s t) = (span s).prod (span t)$$
Lean4
/-- Classification of prime ideals in product rings: the prime ideals of `R × S` are precisely the
ideals of the form `p × S` or `R × p`, where `p` is a prime ideal of `R` or `S`. -/
theorem ideal_prod_prime (I : Ideal (R × S)) :
I.IsPrime ↔ (∃ p : Ideal R, p.IsPrime ∧ I = Ideal.prod p ⊤) ∨ ∃ p : Ideal S, p.IsPrime ∧ I = Ideal.prod ⊤ p :=
by
constructor
· rw [ideal_prod_eq I]
intro hI
rcases ideal_prod_prime_aux hI with (h | h)
· right
rw [h] at hI ⊢
exact ⟨_, ⟨isPrime_of_isPrime_prod_top' hI, rfl⟩⟩
· left
rw [h] at hI ⊢
exact ⟨_, ⟨isPrime_of_isPrime_prod_top hI, rfl⟩⟩
· rintro (⟨p, ⟨h, rfl⟩⟩ | ⟨p, ⟨h, rfl⟩⟩)
· exact isPrime_ideal_prod_top
· exact isPrime_ideal_prod_top'
