chainTopCoeff_of_add — Mathlib

English

If P.root k = P.root j + P.root i, then the top coefficient at k is the sum of j's top and i's bottom offset by one.

Русский

Если P.root k = P.root j + P.root i, то верхний коэффициент цепи на k равен сумме соответствующих коэффициентов j и 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_add {k : ι} (hk : P.root k = P.root j + P.root i) :
    P.chainTopCoeff i j = P.chainTopCoeff i k + 1 :=
  by
  replace h : LinearIndependent R ![P.root i, P.root k] := by rw [hk, add_comm]; simpa
  replace hk : P.root j = P.root k - P.root i := by rw [hk]; abel
  exact chainTopCoeff_of_sub h hk

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