chainTopCoeff_chainTopIdx — Mathlib

English

The root at the chainTopIdx equals root j plus the chainTopCoeff times root i.

Русский

Корень в позиции chainTopIdx равен корню j плюс коэффициент цепи верхнего отношения к корню i.

LaTeX

$$$$ P.root( P.chainTopIdx(i,j) ) = P.root(j) + P.chainTopCoeff(i,j) \cdot P.root(i). $$$$

Lean4

@[simp]
theorem chainTopCoeff_chainTopIdx : P.chainTopCoeff i (P.chainTopIdx i j) = 0 :=
  chainCoeff_chainTopIdx_aux.2

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