chainTopCoeff_le_chainLength — Mathlib

English

The chainTopCoeff α β is always at most the chainLength α β.

Русский

chainTopCoeff α β всегда не превосходит chainLength α β.

LaTeX

$$$\operatorname{chainTopCoeff}(\alpha, \beta) \le \operatorname{chainLength}(\alpha, \beta)$$$

Lean4

theorem chainTopCoeff_le_chainLength : chainTopCoeff α β ≤ chainLength α β :=
  by
  by_cases hα : α.IsZero
  · simp only [hα.eq, chainTopCoeff_zero, zero_le]
  rw [← not_lt, ← Nat.succ_le]
  intro e
  apply genWeightSpace_nsmul_add_ne_bot_of_le α β (Nat.sub_le (chainTopCoeff α β) (chainLength α β).succ)
  rw [← Nat.cast_smul_eq_nsmul ℤ, Nat.cast_sub e, sub_smul, sub_eq_neg_add, add_assoc, ← coe_chainTop,
    Nat.cast_smul_eq_nsmul]
  exact rootSpace_neg_nsmul_add_chainTop_of_lt α β hα (Nat.lt_succ_self _)

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