support_ofFinsupp

Mathlib.Algebra.Polynomial.Basic

URI: https://scilib.ai/kg/mathlib#Polynomial.support_ofFinsupp

English

For any p in AddMonoidAlgebra R Nat, the support of p as a finsupp image equals p.support.

Русский

Для любого p ∈ AddMonoidAlgebra R Nat поддержка p как образ в finsupp равна p.support.

LaTeX

$$$\operatorname{support}(\langle p \rangle) = p.\operatorname{support}$$$

Lean4

@[simp]
theorem support_ofFinsupp (p) : support (⟨p⟩ : R[X]) = p.support := by rw [support]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru