genWeightSpace_chainTopCoeff_add_one_zsmul_add

English

The weight space corresponding to the top coefficient plus one, interpreted via integer scalars, is trivial.

Русский

Весовое пространство верхнего коэффициента плюс единица в целочисленной нотации тривиально.

LaTeX

$$$ genWeightSpace M \\big( (\\text{chainTopCoeff}(\\alpha, \\beta) + 1) \\cdot \\alpha + \\beta \\big) = \\bot $$$

Lean4

theorem genWeightSpace_chainTopCoeff_add_one_zsmul_add :
    genWeightSpace M ((chainTopCoeff α β + 1 : ℤ) • α + β : L → R) = ⊥ := by
  rw [← genWeightSpace_chainTopCoeff_add_one_nsmul_add α β hα, ← Nat.cast_smul_eq_nsmul ℤ, Nat.cast_add, Nat.cast_one]

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