natDegree_nodal

Mathlib.LinearAlgebra.Lagrange

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

← MathLib Explorer

English

The nodal polynomial has degree equal to the size of s.

Русский

Натуральная степень nодал(с,v) равна |s| при поле.

LaTeX

$$$ \\operatorname{natDegree}( \\operatorname{nodal}(s,v) ) = |s|. $$$

Lean4

@[simp]
theorem natDegree_nodal [Nontrivial R] : (nodal s v).natDegree = #s := by
  simp_rw [nodal, natDegree_prod_of_monic (h := fun i _ => monic_X_sub_C (v i)), natDegree_X_sub_C, sum_const,
    smul_eq_mul, mul_one]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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