coprime_of_no_prime_ge — Mathlib

English

If no prime P contains both I and J, then I and J are coprime.

Русский

Если не существует прайм-идеала P, содержащего одновременно I и J, то I и J взаимно просты.

LaTeX

$$$$ (\forall P, I \le P \to J \le P \to \neg P.IsPrime) \Rightarrow IsCoprime I J $$$$

Lean4

theorem coprime_of_no_prime_ge {I J : Ideal R} (h : ∀ P, I ≤ P → J ≤ P → ¬IsPrime P) : IsCoprime I J :=
  by
  rw [isCoprime_iff_sup_eq]
  by_contra hIJ
  obtain ⟨P, hP, hIJ⟩ := Ideal.exists_le_maximal _ hIJ
  exact h P (le_trans le_sup_left hIJ) (le_trans le_sup_right hIJ) hP.isPrime

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