chainTopCoeff_sub_chainBotCoeff — Mathlib

English

The chainTopCoeff i j vanishes iff the roots are not LI or a certain difference lies outside the root range.

Русский

Коэффициент верхней цепи i,j равен нулю тогда и только тогда, когда корни не LI или разность не лежит в диапазоне корней.

LaTeX

$$$$ P.chainTopCoeff(i,j) = 0 \iff \; \neg \text{LinearIndependent}(R, [P.root i, P.root j]) \lor P.root j + P.root i \notin \operatorname{range} P.root $$$$

Lean4

theorem chainTopCoeff_sub_chainBotCoeff : P.chainTopCoeff i j - P.chainBotCoeff i j = -P.pairingIn ℤ j i := by
  rw [← chainBotCoeff_sub_chainTopCoeff h, neg_sub]

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