basisDivisor_eq_zero_iff

Mathlib.LinearAlgebra.Lagrange

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

English

The degree of basisDivisor x x is zero (i.e., constant).

Русский

СтепеньBasisDivisor для x=x равна нулю (константа).

LaTeX

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

Lean4

@[simp]
theorem basisDivisor_eq_zero_iff : basisDivisor x y = 0 ↔ x = y :=
  ⟨basisDivisor_inj, fun H => H ▸ basisDivisor_self⟩

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

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

Разделы

Аффилиация

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