CNF — Mathlib

English

For any b, CNF(b, 0) is the empty list.

Русский

Для любого b CNF(b, 0) — пустой список.

LaTeX

$$$\forall b\; CNF(b, 0) = []$$$

Lean4

/-- The Cantor normal form of an ordinal `o` is the list of coefficients and exponents in the
base-`b` expansion of `o`.

We special-case `CNF 0 o = CNF 1 o = [(0, o)]` for `o ≠ 0`.

`CNF b (b ^ u₁ * v₁ + b ^ u₂ * v₂) = [(u₁, v₁), (u₂, v₂)]` -/
@[pp_nodot]
def _root_.Ordinal.CNF (b o : Ordinal) : List (Ordinal × Ordinal) :=
  CNF.rec b [] (fun o _ IH ↦ (log b o, o / b ^ log b o) :: IH) o

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