norm_num extensions for Ordinals

The default norm_num extensions for many operators requires a semiring, which without a right distributive law, ordinals do not have.

We must therefore define new extensions for them.

theorem Mathlib.Meta.NormNum.isNat_ordinalMul {a b : Ordinal.{u}} {an bn rn : ℕ} : IsNat a an → IsNat b bn → an * bn = rn → IsNat (a * b) rn

def Mathlib.Meta.NormNum.evalOrdinalMul : NormNumExt

The norm_num extension for multiplication on ordinals.

Equations

• One or more equations did not get rendered due to their size.

theorem Mathlib.Meta.NormNum.isNat_ordinalLE_true {a b : Ordinal.{u}} {an bn : ℕ} : IsNat a an → IsNat b bn → decide (an ≤ bn) = true → a ≤ b

theorem Mathlib.Meta.NormNum.isNat_ordinalLE_false {a b : Ordinal.{u}} {an bn : ℕ} : IsNat a an → IsNat b bn → decide (an ≤ bn) = false → ¬a ≤ b

theorem Mathlib.Meta.NormNum.isNat_ordinalLT_true {a b : Ordinal.{u}} {an bn : ℕ} : IsNat a an → IsNat b bn → decide (an < bn) = true → a < b

theorem Mathlib.Meta.NormNum.isNat_ordinalLT_false {a b : Ordinal.{u}} {an bn : ℕ} : IsNat a an → IsNat b bn → decide (an < bn) = false → ¬a < b

def Mathlib.Meta.NormNum.evalOrdinalLE : NormNumExt

The norm_num extension for inequality on ordinals.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.NormNum.evalOrdinalLT : NormNumExt

The norm_num extension for strict inequality on ordinals.

Equations

• One or more equations did not get rendered due to their size.

theorem Mathlib.Meta.NormNum.isNat_ordinalSub {a b : Ordinal.{u}} {an bn rn : ℕ} : IsNat a an → IsNat b bn → an - bn = rn → IsNat (a - b) rn

def Mathlib.Meta.NormNum.evalOrdinalSub : NormNumExt

The norm_num extension for subtraction on ordinals.

Equations

• One or more equations did not get rendered due to their size.

theorem Mathlib.Meta.NormNum.isNat_ordinalDiv {a b : Ordinal.{u}} {an bn rn : ℕ} : IsNat a an → IsNat b bn → an / bn = rn → IsNat (a / b) rn

def Mathlib.Meta.NormNum.evalOrdinalDiv : NormNumExt

The norm_num extension for division on ordinals.

Equations

• One or more equations did not get rendered due to their size.

theorem Mathlib.Meta.NormNum.isNat_ordinalMod {a b : Ordinal.{u}} {an bn rn : ℕ} : IsNat a an → IsNat b bn → an % bn = rn → IsNat (a % b) rn

def Mathlib.Meta.NormNum.evalOrdinalMod : NormNumExt

The norm_num extension for modulo on ordinals.

Equations

• One or more equations did not get rendered due to their size.

theorem Mathlib.Meta.NormNum.isNat_ordinalOPow {a b : Ordinal.{u}} {an bn rn : ℕ} : IsNat a an → IsNat b bn → an ^ bn = rn → IsNat (a ^ b) rn

def Mathlib.Meta.NormNum.evalOrdinalOPow : NormNumExt

The norm_num extension for homogeneous power on ordinals.

Equations

• One or more equations did not get rendered due to their size.

theorem Mathlib.Meta.NormNum.isNat_ordinalNPow {a : Ordinal.{u}} {b an bn rn : ℕ} : IsNat a an → IsNat b bn → an ^ bn = rn → IsNat (a ^ b) rn

def Mathlib.Meta.NormNum.evalOrdinalNPow : NormNumExt

The norm_num extension for natural power on ordinals.

Equations

• One or more equations did not get rendered due to their size.