basisDivisor_inj

Mathlib.LinearAlgebra.Lagrange

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

← MathLib Explorer

English

If x ≠ y, then the basis divisor basisDivisor(x,y) has degree 1.

Русский

Если x ≠ y, то базисный делитель basisDivisor(x,y) имеет степень 1.

LaTeX

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

Lean4

theorem basisDivisor_inj (hxy : basisDivisor x y = 0) : x = y :=
  by
  simp_rw [basisDivisor, mul_eq_zero, X_sub_C_ne_zero, or_false, C_eq_zero, inv_eq_zero, sub_eq_zero] at hxy
  exact hxy

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

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

Разделы

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

Аффилиация

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