chainBotCoeff_of_eq_zsmul_add — Mathlib

English

The chainTopCoeff α 0 equals 1 for nonzero α and nontrivial L.

Русский

Для ненулевого α и нетривиального L, chainTopCoeff α 0 = 1.

LaTeX

$$$\operatorname{chainTopCoeff}(α, 0) = 1$$$

Lean4

theorem chainBotCoeff_of_eq_zsmul_add (hα : α.IsNonZero) (β' : Weight K H L) (n : ℤ) (hβ' : (β' : H → K) = n • α + β) :
    chainBotCoeff α β' = chainBotCoeff α β + n :=
  by
  have : (β' : H → K) = -n • (-α) + β := by rwa [neg_smul, smul_neg, neg_neg]
  rw [chainBotCoeff, chainBotCoeff, ← Weight.coe_neg, chainTopCoeff_of_eq_zsmul_add (-α) β hα.neg β' (-n) this,
    sub_neg_eq_add]

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