root_chainBotIdx — Mathlib

English

The top coefficient after applying the reflection permutation on j equals the bottom coefficient with i and j fixed.

Русский

Верхний коэффициент после применения отражения к j равен нижнему коэффициенту при фиксированных i, j.

LaTeX

$$$$ P.chainTopCoeff(i, P.reflectionPerm(j,j)) = P.chainBotCoeff(i, j) $$$$

Lean4

@[simp]
theorem root_chainBotIdx : P.root (P.chainBotIdx i j) = P.root j - P.chainBotCoeff i j • P.root i :=
  by
  by_cases h : LinearIndependent R ![P.root i, P.root j]
  · simp only [chainBotIdx, reduceDIte, h]
    exact (P.root_sub_nsmul_mem_range_iff_le_chainBotCoeff h).mpr (le_refl <| P.chainBotCoeff i j) |>.choose_spec
  · simp only [chainBotIdx, chainBotCoeff, h, reduceDIte, zero_smul, sub_zero]

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