support_toFinsupp — Mathlib

English

Let p be a polynomial over a semiring R. The nonzero terms of p coincide with the nonzero terms of p viewed as a finsupp, i.e. the support of p is equal to the support of p.toFinsupp.

Русский

Пусть p — полином над полем R. Ненулевые члены p совпадают с ненулевыми членами представления p в виде finsupp, то есть поддержка p равна поддержке p.toFinsupp.

LaTeX

$$$\operatorname{supp}(p^{\mathrm{toFinsupp}}) = \operatorname{supp}(p)$$$

Lean4

theorem support_toFinsupp (p : R[X]) : p.toFinsupp.support = p.support := by rw [support]

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