chainLength_of_eq_zsmul_add — Mathlib

English

A corollary states equality of chainTopCoeff with 1 in the zero-chain scenario under nontrivial assumptions.

Русский

Следствие данных условий даёт равенство chainTopCoeff с 1 в нулевой цепи.

LaTeX

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

Lean4

theorem chainLength_of_eq_zsmul_add (β' : Weight K H L) (n : ℤ) (hβ' : (β' : H → K) = n • α + β) :
    chainLength α β' = chainLength α β := by
  by_cases hα : α.IsZero
  · rw [chainLength_of_isZero _ _ hα, chainLength_of_isZero _ _ hα]
  · apply Nat.cast_injective (R := ℤ)
    rw [← chainTopCoeff_add_chainBotCoeff, ← chainTopCoeff_add_chainBotCoeff, Nat.cast_add, Nat.cast_add,
      chainTopCoeff_of_eq_zsmul_add α β hα β' n hβ', chainBotCoeff_of_eq_zsmul_add α β hα β' n hβ', sub_eq_add_neg,
      add_add_add_comm, neg_add_cancel, add_zero]

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