chainTopCoeff_add_chainBotCoeff — Mathlib

English

The sum of chainBotCoeff and chainTopCoeff equals the total chainLength: chainBotCoeff α β + chainTopCoeff α β = chainLength α β.

Русский

Сумма chainBotCoeff и chainTopCoeff равна общей длине цепи: chainBotCoeff α β + chainTopCoeff α β = chainLength α β.

LaTeX

$$$\operatorname{chainBotCoeff}(\alpha, \beta) + \operatorname{chainTopCoeff}(\alpha, \beta) = \operatorname{chainLength}(\alpha, \beta)$$$

Lean4

theorem chainTopCoeff_add_chainBotCoeff : chainTopCoeff α β + chainBotCoeff α β = chainLength α β := by
  rw [add_comm, chainBotCoeff_add_chainTopCoeff]

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