chainTopCoeff_of_eq_zsmul_add — Mathlib

English

The chainTopCoeff is bounded above by the chainLength for all α, β in a triangularizable setting.

Русский

chainTopCoeff ограничена сверху chainLength для любых (α,β) в условиях треугольной совместимости.

LaTeX

$$$\operatorname{chainTopCoeff}(α,β) \le \operatorname{chainLength}(α,β)$$$

Lean4

theorem chainTopCoeff_of_eq_zsmul_add (hα : α.IsNonZero) (β' : Weight K H L) (n : ℤ) (hβ' : (β' : H → K) = n • α + β) :
    chainTopCoeff α β' = chainTopCoeff α β - n := by
  apply le_antisymm
  · refine le_sub_iff_add_le.mpr ((rootSpace_zsmul_add_ne_bot_iff α β hα _).mp ?_).1
    rw [add_smul, add_assoc, ← hβ', ← coe_chainTop]
    exact (chainTop α β').2
  · refine ((rootSpace_zsmul_add_ne_bot_iff α β' hα _).mp ?_).1
    rw [hβ', ← add_assoc, ← add_smul, sub_add_cancel, ← coe_chainTop]
    exact (chainTop α β).2

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