root_chainTopIdx — Mathlib

English

The root corresponding to chainTopIdx equals the root j plus the chainTopCoeff times the root i.

Русский

Корень, соответствующий chainTopIdx, равен корню j плюс coefficient вершины цепи, умноженный на корень i.

LaTeX

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

Lean4

@[simp]
theorem root_chainTopIdx : P.root (P.chainTopIdx i j) = P.root j + P.chainTopCoeff i j • P.root i :=
  by
  by_cases h : LinearIndependent R ![P.root i, P.root j]
  · simp only [chainTopIdx, reduceDIte, h]
    exact (P.root_add_nsmul_mem_range_iff_le_chainTopCoeff h).mpr (le_refl <| P.chainTopCoeff i j) |>.choose_spec
  · simp only [chainTopIdx, chainTopCoeff, h, reduceDIte, zero_smul, add_zero]

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