rootSpace_zsmul_add_ne_bot_iff_mem

English

If α is nonzero and chainLength α β is greater than n, then the root space at -(n•α) + chainTop α β is nontrivial.

Русский

Если α ≠ 0 и chainLength α β > n, тогда пространство корня по -(nα) + chainTop α β не тривиально.

LaTeX

$$$n < \operatorname{chainLength}(α,β) \Rightarrow \operatorname{rootSpace}(H, -(n \cdot α) + \operatorname{chainTop}(α,β)) \neq ⊥$$$

Lean4

theorem rootSpace_zsmul_add_ne_bot_iff_mem (hα : α.IsNonZero) (n : ℤ) :
    rootSpace H (n • α + β) ≠ ⊥ ↔ n ∈ Finset.Icc (-chainBotCoeff α β : ℤ) (chainTopCoeff α β) := by
  rw [rootSpace_zsmul_add_ne_bot_iff α β hα n, Finset.mem_Icc, and_comm, neg_le]

Похожие утверждения