mem_coeffs_iff — Mathlib

English

For any polynomial p and coefficient c, c is a coefficient of p if and only if there exists a monomial index n appearing in p with c equal to p.coeff n.

Русский

Для любого полинома p и коэффициента c выполняется: c является коэффициентом p тогда и только тогда, когда существует индекс мономиального члена n, входящего в p, такой что c = p.coeff n.

LaTeX

$$$ \\forall p : \\mathrm{MvPolynomial}(\\sigma, R), \\forall c : R, c \\in p.\\mathrm{coeffs} \\iff \\exists n \\in p.\\mathrm{support}, c = p.\\mathrm{coeff} n. $$$

Lean4

theorem mem_coeffs_iff {p : MvPolynomial σ R} {c : R} : c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = p.coeff n := by
  simp [coeffs, eq_comm, (Finset.mem_image)]

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