Mathlib Map

Structures · Logic and sets

ONote.NF

A normal form ordinal notation has the form ω ^ a₁ * n₁ + ω ^ a₂ * n₂ + ⋯ + ω ^ aₖ * nₖ where a₁ > a₂ > ⋯ > aₖ and all the aᵢ are also in normal form. We will essentially only be interested in normal form ordinal notations, but to avoid complicating the algorithms, we define everything over general ordinal notations and only prove correctness with normal form as an invariant.

Defined in
Mathlib.SetTheory.Ordinal.Notation
Shape
One type argument · adds out
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by0

Nothing extends this class yet.

Concrete types that are instances11

  • OfNat.ofNat
  • HAdd.hAdd
  • ONote.mulNat
  • HMul.hMul
  • ONote.ofNat
  • ONote.opowAux
  • ONote.oadd
  • ONote.scale
  • HSub.hSub
  • Subtype.val
  • HPow.hPow

How is a type an instance?

Loading the hierarchy index…

Assumed by26

Ancestors0

No ancestors.