English
Let P be crystallographic and the roots P.root i, P.root j be independent. Then the bottom chain coefficient satisfies a similar supremum description, namely it is the supremum of integers k for which P.root j minus k times P.root i lies in the root range.
Русский
Пусть P — кристаллическое, и корни P.root i, P.root j линейно независимы. Тогда нижний коэффициент цепи описывается как верхняя грань множества целых k, для которых P.root j минус k·P.root i принадлежит диапазону корней.
LaTeX
$$$$ P\text{.chainBotCoeff}(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_chainBotCoeff_eq_sSup : P.chainBotCoeff i j = sSup {k : ℤ | P.root j - k • P.root i ∈ range P.root} :=
by
rw [setOf_root_sub_zsmul_mem_eq_Icc h]
simp
