mem_coeffs_iff — Mathlib

English

An element c belongs to the coefficients of p if and only if there exists an index n in the support of p with c = p.coeff n.

Русский

Элемент c принадлежит коэффициентам p если и только если существует индекс n, принадлежащий опоре p, такой что c = p.coeff n.

LaTeX

$$$c \\in p.coeffs \\iff \\exists n \\in p.support,\\ c = p.coeff n$$$

Lean4

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

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