chainTopCoeff_of_sub — Mathlib

English

If hk expresses P.root k as P.root j minus P.root i, then the top coefficient transforms by a plus-one rule.

Русский

Если hk задаёт P.root k = P.root j − P.root i, то верхний коэффициент изменяется по правилу плюс один.

LaTeX

$$$$ P.chainTopCoeff(i, k) = P.chainTopCoeff(i, j) + 1 \quad\text{when}\quad P.root(k) = P.root(j) - P.root(i). $$$$

Lean4

theorem chainTopCoeff_of_sub {k : ι} (hk : P.root k = P.root j - P.root i) :
    P.chainTopCoeff i k = P.chainTopCoeff i j + 1 :=
  by
  letI := P.indexNeg
  replace hk : P.root k = P.root j + P.root (-i) := by simpa [sub_eq_add_neg] using hk
  simpa using chainBotCoeff_of_add (by simpa) hk

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