apply_coroot_eq_cast — Mathlib

English

The coroot evaluation β(coroot α) equals chainBotCoeff α β minus chainTopCoeff α β, interpreted as an integer: β(coroot α) = (chainBotCoeff α β − chainTopCoeff α β) in ℤ, then embedded in the base field.

Русский

Оценка β на коротe α равна chainBotCoeff α β минус chainTopCoeff α β, как целое число и затем введённое в базовое поле.

LaTeX

$$$\beta(\mathrm{coroot}(\alpha)) = (\operatorname{chainBotCoeff}(\alpha, \beta) - \operatorname{chainTopCoeff}(\alpha, \beta) : \mathbb{Z})$$$

Lean4

/-- If `β - qα ... β ... β + rα` is the `α`-chain through `β`, then
  `β (coroot α) = q - r`. In particular, it is an integer. -/
theorem apply_coroot_eq_cast : β (coroot α) = (chainBotCoeff α β - chainTopCoeff α β : ℤ) := by
  rw [apply_coroot_eq_cast', ← chainTopCoeff_add_chainBotCoeff]; congr 1; cutsat

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