coeff_mem_coeffs — Mathlib

English

For a semiring R and a polynomial p, if the nth coefficient p.coeff n is nonzero, then p.coeff n belongs to the coefficient set p.coeffs.

Русский

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

LaTeX

$$$p.coeff\,n \in p.coeffs$$$

Lean4

theorem coeff_mem_coeffs {p : R[X]} {n : ℕ} (h : p.coeff n ≠ 0) : p.coeff n ∈ p.coeffs := by
  classical
  simp only [coeffs, mem_support_iff, Finset.mem_image, Ne]
  exact ⟨n, h, rfl⟩

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