English
The bottom chain coefficient vanishes iff the roots are not linearly independent or a certain root difference is outside the root range.
Русский
Нижний коэффициент цепи равен нулю тогда и только тогда, когда корни линейно зависимы или разность корней выходит за пределы диапазона корней.
LaTeX
$$$$ P.chainBotCoeff(i, j) = 0 \iff \; \neg \text{LinearIndependent}(R, [P.root i, P.root j]) \; \lor\; P.root \\ j - P.root \\ i \notin \operatorname{range} P.root $$$$
Lean4
theorem chainBotCoeff_eq_zero_iff :
P.chainBotCoeff i j = 0 ↔ ¬LinearIndependent R ![P.root i, P.root j] ∨ P.root j - P.root i ∉ range P.root :=
by
by_cases h : LinearIndependent R ![P.root i, P.root j]
swap; · simp [chainBotCoeff_of_not_linearIndependent h, h]
have : P.chainBotCoeff i j = 0 ↔ Iic (P.chainBotCoeff i j) = {0} := by
simpa [Set.ext_iff, mem_Iic, mem_singleton_iff] using ⟨fun h ↦ by simp [h], fun h ↦ by rw [← h]⟩
simp only [h, not_true_eq_false, false_or, this, Iic_chainBotCoeff_eq h, Set.ext_iff, mem_setOf_eq, mem_singleton_iff]
refine ⟨fun h' ↦ by simpa using h' 1, fun h' n ↦ ⟨fun h'' ↦ ?_, fun h'' ↦ by simp [h'']⟩⟩
replace h' : 1 ∉ {k | P.root j - k • P.root i ∈ range P.root} := by simpa using h'
rw [← Iic_chainBotCoeff_eq h, mem_Iic, not_le, Nat.lt_one_iff] at h'
rw [root_sub_nsmul_mem_range_iff_le_chainBotCoeff h] at h''
cutsat
