natDegree_basisDivisor_self

Mathlib.LinearAlgebra.Lagrange

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

English

The natDegree of basisDivisor x x is 0.

Русский

NatDegree basisDivisor x x равно 0.

LaTeX

$$$$\\operatorname{natDegree}(\\text{basisDivisor}(x,x)) = 0.$$$$

Lean4

theorem natDegree_basisDivisor_self : (basisDivisor x x).natDegree = 0 := by rw [basisDivisor_self, natDegree_zero]

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

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

Разделы

Аффилиация

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