English
If α is nonzero and there is a nonempty chain-top coefficient relation, then n lies in the integer interval determined by chainTopCoeff and chainBotCoeff.
Русский
Если α ≠ 0 и существует отношение в цепочке верхних коэффициентов, то n лежит в целочисленном интервале между chainTopCoeff и chainBotCoeff.
LaTeX
$$See corresponding lemma: n ∈ [−chainBotCoeff α β, chainTopCoeff α β].$$
Lean4
/-- Members of the `α`-chain through `β` are the only roots of the form `β - kα`. -/
theorem rootSpace_zsmul_add_ne_bot_iff (hα : α.IsNonZero) (n : ℤ) :
rootSpace H (n • α + β) ≠ ⊥ ↔ n ≤ chainTopCoeff α β ∧ -n ≤ chainBotCoeff α β :=
by
constructor
· refine (fun hn ↦ ⟨?_, le_chainBotCoeff_of_rootSpace_ne_top α β hα _ (by rwa [neg_neg])⟩)
rw [← chainBotCoeff_neg, ← Weight.coe_neg]
apply le_chainBotCoeff_of_rootSpace_ne_top _ _ hα.neg
rwa [neg_smul, Weight.coe_neg, smul_neg, neg_neg]
· rintro ⟨h₁, h₂⟩
set k := chainTopCoeff α β - n with hk; clear_value k
lift k to ℕ using (by rw [hk, le_sub_iff_add_le, zero_add]; exact h₁)
rw [eq_sub_iff_add_eq, ← eq_sub_iff_add_eq'] at hk
subst hk
simp only [neg_sub, tsub_le_iff_right, ← Nat.cast_add, Nat.cast_le, chainBotCoeff_add_chainTopCoeff] at h₂
have := rootSpace_neg_nsmul_add_chainTop_of_le α β h₂
rwa [coe_chainTop, ← Nat.cast_smul_eq_nsmul ℤ, ← neg_smul, ← add_assoc, ← add_smul, ← sub_eq_neg_add] at this
