coeffs_empty_iff — Mathlib

English

For a polynomial p, coeffs(p) = ∅ if and only if p = 0.

Русский

Для многочлена p множество коэффициентов пустое тогда и только тогда, когда p = 0.

LaTeX

$$$\operatorname{coeffs}(p) = \emptyset \iff p = 0$$$

Lean4

@[simp]
theorem coeffs_empty_iff {p : R[X]} : coeffs p = ∅ ↔ p = 0 :=
  by
  refine ⟨?_, fun h ↦ by simp [h]⟩
  contrapose!
  intro h
  rw [← support_nonempty] at h
  obtain ⟨n, hn⟩ := h
  rw [mem_support_iff] at hn
  rw [← nonempty_iff_ne_empty]
  exact ⟨p.coeff n, coeff_mem_coeffs hn⟩

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