contentIdeal_eq_top_of_contentIdeal_mul_eq_top

English

If the content ideal of p q equals top, then p.contentIdeal equals top.

Русский

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

LaTeX

$$ (p \cdot q).contentIdeal = \top \Rightarrow p.contentIdeal = \top$$

Lean4

theorem contentIdeal_eq_top_of_contentIdeal_mul_eq_top (h : (p * q).contentIdeal = ⊤) : p.contentIdeal = ⊤ :=
  by
  apply le_antisymm le_top
  calc
    ⊤ = (p * q).contentIdeal := h.symm
    _ ≤ p.contentIdeal * q.contentIdeal := (contentIdeal_mul_le_mul_contentIdeal p q)
    _ ≤ p.contentIdeal := mul_le_right

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