toFn_zero

Mathlib.Algebra.Polynomial.OfFn

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

English

For every n, toFn(n) applied to the zero polynomial is the zero vector.

Русский

Для каждого n отображение toFn(n) от нулевого многочлена даёт нулевой вектор.

LaTeX

$$$\operatorname{toFn}(n)(0) = 0$.$$

Lean4

theorem toFn_zero (n : ℕ) : toFn n (0 : R[X]) = 0 := by simp

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

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

Разделы

Аффилиация

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