basisDivisor_ne_zero_iff

Mathlib.LinearAlgebra.Lagrange

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

English

If x ≠ y, then the natDegree of basisDivisor(x,y) is 1.

Русский

Если x ≠ y, то natDegree basisDivisor(x,y) равно 1.

LaTeX

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

Lean4

theorem basisDivisor_ne_zero_iff : basisDivisor x y ≠ 0 ↔ x ≠ y := by rw [Ne, basisDivisor_eq_zero_iff]

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

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

Разделы

Аффилиация

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