mul_contentIdeal_le_radical_contentIdeal_mul

English

If p.contentIdeal = ⊤ and q.contentIdeal = ⊤, then (p q).contentIdeal = ⊤.

Русский

Если contentIdeal(p) = ⊤ и contentIdeal(q) = ⊤, то contentIdeal(p q) = ⊤.

LaTeX

$$(p.contentIdeal = \top) ∧ (q.contentIdeal = \top) ⇒ (p \cdot q).contentIdeal = \top$$

Lean4

theorem mul_contentIdeal_le_radical_contentIdeal_mul :
    p.contentIdeal * q.contentIdeal ≤ ((p * q).contentIdeal).radical :=
  by
  rw [radical_eq_sInf, le_sInf_iff]
  intro P ⟨hpq, hPprime⟩
  rw [hPprime.mul_le]
  rw [← Ideal.mk_ker (I := P)] at hpq ⊢
  simpa only [← map_eq_bot_iff_le_ker, ← contentIdeal_map_eq_map_contentIdeal, Polynomial.map_mul,
    contentIdeal_eq_bot_iff, mul_eq_zero] using hpq

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