le_chainBotCoeff_of_rootSpace_ne_top

English

If α is nonzero and there is a nontrivial root space at -(n•α) + β with n in ℤ, then n ≤ chainBotCoeff α β.

Русский

Если α ненулевой и существует нетривиальное пространство корня для -(n•α) + β, то n ≤ chainBotCoeff α β.

LaTeX

$$$\text{rootSpace}(H, -n \cdot α + β) \neq ⊥ \Rightarrow n \le \operatorname{chainBotCoeff}(α, β)$$$

Lean4

theorem le_chainBotCoeff_of_rootSpace_ne_top (hα : α.IsNonZero) (n : ℤ) (hn : rootSpace H (-n • α + β) ≠ ⊥) :
    n ≤ chainBotCoeff α β := by
  contrapose! hn
  lift n to ℕ using (Nat.cast_nonneg _).trans hn.le
  rw [Nat.cast_lt, ← @Nat.add_lt_add_iff_right (chainTopCoeff α β), chainBotCoeff_add_chainTopCoeff] at hn
  have := rootSpace_neg_nsmul_add_chainTop_of_lt α β hα hn
  rwa [← Nat.cast_smul_eq_nsmul ℤ, ← neg_smul, coe_chainTop, ← add_assoc, ← add_smul, Nat.cast_add, neg_add, add_assoc,
    neg_add_cancel, add_zero] at this

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