natDegree_basisDivisor_of_ne

Mathlib.LinearAlgebra.Lagrange

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

← MathLib Explorer

English

If x ≠ y, natDegree of basisDivisor x y is 1.

Русский

Если x ≠ y, natDegree basisDivisor x y равен 1.

LaTeX

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

Lean4

theorem natDegree_basisDivisor_of_ne (hxy : x ≠ y) : (basisDivisor x y).natDegree = 1 :=
  natDegree_eq_of_degree_eq_some (degree_basisDivisor_of_ne hxy)

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

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

Разделы

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

Аффилиация

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