content_eq_zero_iff — Mathlib

English

For a polynomial p over a domain, content p = 0 if and only if p = 0.

Русский

Для полинома p над областью содержимое p равно нулю тогда и только тогда, когда p = 0.

LaTeX

$$$$ content(p) = 0 \\iff p = 0 $$$$

Lean4

theorem content_eq_zero_iff {p : R[X]} : content p = 0 ↔ p = 0 :=
  by
  rw [content, Finset.gcd_eq_zero_iff]
  constructor <;> intro h
  · ext n
    by_cases h0 : n ∈ p.support
    · rw [h n h0, coeff_zero]
    · rw [mem_support_iff] at h0
      push_neg at h0
      simp [h0]
  · intro x
    simp [h]
      -- `simp`-normal form is `normUnit_content`

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