chainLength — Mathlib

English

Define the length of an α-chain through β in the Killing context; it is zero if α is zero, otherwise it is the successor of the top coefficient determined by the chainTop.

Русский

Определим длину цепи α через β в контексте Каррана; она равна нулю, если α=0, иначе — продолжение топ-коэффициента, полученного через chainTop.

LaTeX

$$$\\mathrm{chainLength}(α,β) = 0 \\text{ if } α=0,\; \\text{ otherwise given by chainTop and existence of a nonzero α-chain.}$$$

Lean4

/-- The length of the `α`-chain through `β`. See `chainBotCoeff_add_chainTopCoeff`. -/
def chainLength (α β : Weight K H L) : ℕ :=
  letI := Classical.propDecidable
  if hα : α.IsZero then 0 else (chainLength_aux α β hα (chainTop α β).exists_ne_zero.choose_spec.1).choose

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