English
Let P be a crystallographic RootPairing with independent roots P.root i and P.root j. Then the top chain coefficient between i and j is the supremum of all integers k such that the root j plus k times the root i lies in the image of the root map.
Русский
Пусть P — кристаллическое RootPairing, и корни P.root i и P.root j линейно независимы. Тогда верхний коэффициент цепи между i и j равен верхней грань множества целых чисел k, для которых корень j плюс k раз корень i принадлежит образу отображения корней.
LaTeX
$$$$ P\text{.chainTopCoeff}(i, j) = \operatorname{sSup}\{ k \in \mathbb{Z} \mid P.root(j) + k \cdot P.root(i) \in \operatorname{range} P.root\} $$$$
Lean4
theorem coe_chainTopCoeff_eq_sSup : P.chainTopCoeff i j = sSup {k : ℤ | P.root j + k • P.root i ∈ range P.root} :=
by
rw [setOf_root_add_zsmul_mem_eq_Icc h]
simp
