contentIdeal_mul_eq_top_of_contentIdeal_eq_top

English

Same as above: if p.contentIdeal = ⊤ and q.contentIdeal = ⊤, then (p q).contentIdeal = ⊤.

Русский

То же самое: если contentIdeal(p) = ⊤ и contentIdeal(q) = ⊤, тогда (p q).contentIdeal = ⊤.

LaTeX

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

Lean4

theorem contentIdeal_mul_eq_top_of_contentIdeal_eq_top (hp : p.contentIdeal = ⊤) (hq : q.contentIdeal = ⊤) :
    (p * q).contentIdeal = ⊤ := by
  rw [← Ideal.radical_eq_top]
  apply le_antisymm le_top
  calc
    ⊤ = p.contentIdeal * q.contentIdeal := by simp [hp, hq]
    _ ≤ ((p * q).contentIdeal).radical := mul_contentIdeal_le_radical_contentIdeal_mul

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