English
For α nonzero, there is an equivalence between rootSpace at n•α + β being nontrivial and n belonging to the finite set determined by coefficients of α and β.
Русский
Для α ≠ 0 существует эквивалентность: корневое пространство при n•α + β не тривиально тогда и только тогда, когда n принадлежит конечному множеству, определяемому коэффициентами α и β.
LaTeX
$$$\text{rootSpace}(H, n·α + β) \neq ⊥ \iff n ∈ \mathrm{Finset.Icc}(-\operatorname{chainBotCoeff}(α,β), \operatorname{chainTopCoeff}(α,β))$$$
Lean4
/-- `±α` are the only `K`-multiples of a root `α` that are also (non-zero) roots. -/
theorem eq_neg_or_eq_of_eq_smul (hβ : β.IsNonZero) (k : K) (h : (β : H → K) = k • α) : β = -α ∨ β = α :=
by
by_cases hα : α.IsZero
· rw [hα, smul_zero] at h; cases hβ h
rcases eq_neg_one_or_eq_zero_or_eq_one_of_eq_smul α β hα k h with (rfl | rfl | rfl)
· exact .inl (by ext; rw [h, neg_one_smul]; rfl)
· cases hβ (by rwa [zero_smul] at h)
· exact .inr (by ext; rw [h, one_smul])
