chainTopCoeff_eq_zero_iff — Mathlib

English

Symmetric criterion for the vanishing of the top chain coefficient: zero occurs iff not LI or an analogue of the sum condition fails.

Русский

Симметричный критерий нуля для верхнего коэффициента цепи: ноль происходит либо при не линейной независимости, либо при нарушении соответствующего условия суммы.

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_eq_zero_iff :
    P.chainTopCoeff i j = 0 ↔ ¬LinearIndependent R ![P.root i, P.root j] ∨ P.root j + P.root i ∉ range P.root :=
  by
  rw [← chainBotCoeff_reflectionPerm_left]
  simp [-chainBotCoeff_reflectionPerm_left, chainBotCoeff_eq_zero_iff]

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