le_mul_of_no_prime_factors — Mathlib

English

Variant of le_mul_of_no_prime_factors with a different ordering convention.

Русский

Вариант le_mul_of_no_prime_factors с другой перестановкой приоритетов.

LaTeX

$$le_mul_of_no_prime_factors$$

Lean4

theorem le_mul_of_no_prime_factors {I J K : Ideal R} (coprime : ∀ P, J ≤ P → K ≤ P → ¬IsPrime P) (hJ : I ≤ J)
    (hK : I ≤ K) : I ≤ J * K := by
  simp only [← Ideal.dvd_iff_le] at coprime hJ hK ⊢
  by_cases hJ0 : J = 0
  · simpa only [hJ0, zero_mul] using hJ
  obtain ⟨I', rfl⟩ := hK
  rw [mul_comm]
  refine mul_dvd_mul_left K (UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors (b := K) hJ0 ?_ hJ)
  exact fun hPJ hPK => mt Ideal.isPrime_of_prime (coprime _ hPJ hPK)

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