ofFinsupp_single

Mathlib.Algebra.Polynomial.Basic

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

English

The polynomial corresponding to the finsupp singleton is the monomial.

Русский

Полином, соответствующий единичному элементу finsupp, есть мономиал.

LaTeX

$$$\langle \operatorname{Finsupp}.single(n,r) \rangle = \operatorname{monomial}(n,r)$$$

Lean4

@[simp]
theorem ofFinsupp_single (n : ℕ) (r : R) : (⟨Finsupp.single n r⟩ : R[X]) = monomial n r := by simp [monomial]

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

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

Разделы

Аффилиация

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