English
If two indices i,i1 and j,j1 are pairwise equal, then chainTopIdx(i,j) equals chainTopIdx(i1,j1).
Русский
Если i равно i1 и j равно j1 параллельно, то chainTopIdx(i,j) равно chainTopIdx(i1,j1).
LaTeX
$$$$ \text{chainTopIdx}(i,j) = \text{chainTopIdx}(i_1,j_1) \quad\text{whenever } i=i_1 \text{ and } j=j_1. $$$$
Lean4
/-- If `α = P.root i` and `β = P.root j` are linearly independent, this is the index of the root
`β - q • α` where `β - q • α, ..., β - α, β, β + α, ..., β + p • α` is the `α`-chain through `β`.
In the absence of linear independence, it takes a junk value. -/
def chainBotIdx : ι :=
if h : LinearIndependent R ![P.root i, P.root j] then
(P.root_sub_nsmul_mem_range_iff_le_chainBotCoeff h).mpr (le_refl <| P.chainBotCoeff i j) |>.choose
else j
