degree_basisDivisor_self

Mathlib.LinearAlgebra.Lagrange

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

English

Evaluating basisDivisor at y yields 0.

Русский

Значение basisDivisor в точке y равно 0.

LaTeX

$$$$\\mathrm{eval}_y(\\mathrm{basisDivisor}(x,y)) = 0.$$$$

Lean4

@[simp]
theorem degree_basisDivisor_self : (basisDivisor x x).degree = ⊥ := by rw [basisDivisor_self, degree_zero]

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

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

Разделы

Аффилиация

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