English
If n ∈ ℤ satisfies −chainBotCoeff α β ≤ n ≤ chainTopCoeff α β, then genWeightSpace M (n·α + β) ≠ ⊥.
Русский
Если целое число n удовлетворяет −chainBotCoeff α β ≤ n ≤ chainTopCoeff α β, то genWeightSpace M (n·α + β) ≠ ⊥.
LaTeX
$$$ n \\in \\mathbb{Z}, \\; -\\text{chainBotCoeff}(α, β) \\le n \\le \\text{chainTopCoeff}(α, β) \\Rightarrow genWeightSpace M (n·α + β) \\neq \\bot $$$
Lean4
theorem genWeightSpace_zsmul_add_ne_bot {n : ℤ} (hn : -chainBotCoeff α β ≤ n) (hn' : n ≤ chainTopCoeff α β) :
genWeightSpace M (n • α + β : L → R) ≠ ⊥ := by
rcases n with (n | n)
· simp only [Int.ofNat_eq_coe, Nat.cast_le, Nat.cast_smul_eq_nsmul] at hn' ⊢
exact genWeightSpace_nsmul_add_ne_bot_of_le α β hn'
· simp only [Int.negSucc_eq, ← Nat.cast_succ, neg_le_neg_iff, Nat.cast_le] at hn ⊢
rw [neg_smul, ← smul_neg, Nat.cast_smul_eq_nsmul]
exact genWeightSpace_nsmul_add_ne_bot_of_le (-α) β hn
