degree_nodal

Mathlib.LinearAlgebra.Lagrange

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

English

The degree matches the number of nodes.

Русский

В неабельном кольце deg nodal(s,v) = |s|.

LaTeX

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

Lean4

@[simp]
theorem degree_nodal [Nontrivial R] : (nodal s v).degree = #s := by
  simp_rw [degree_eq_natDegree nodal_ne_zero, natDegree_nodal]

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

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

Разделы

Аффилиация

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