nodal_monic

Mathlib.LinearAlgebra.Lagrange

URI: https://scilib.ai/kg/mathlib#Lagrange.nodal_monic

English

Nodal is monic for any finite s.

Русский

Нодальный полином моноичен.

LaTeX

$$$ \\operatorname{nodal}(s,v) \\text{ is Monic}. $$$

Lean4

theorem nodal_monic : (nodal s v).Monic :=
  monic_prod_of_monic s (fun i ↦ X - C (v i)) fun i _ ↦ monic_X_sub_C (v i)

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

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

Разделы

Аффилиация

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