Documentation

Mathlib.Tactic.NormNum.Ordinal

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 anIsNat b bnan * bn = rnIsNat (a * b) rn

The norm_num extension for multiplication on ordinals.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem Mathlib.Meta.NormNum.isNat_ordinalLE_true {a b : Ordinal.{u}} {an bn : } :
    IsNat a anIsNat b bndecide (an bn) = truea b
    theorem Mathlib.Meta.NormNum.isNat_ordinalLE_false {a b : Ordinal.{u}} {an bn : } :
    IsNat a anIsNat b bndecide (an bn) = false¬a b
    theorem Mathlib.Meta.NormNum.isNat_ordinalLT_true {a b : Ordinal.{u}} {an bn : } :
    IsNat a anIsNat b bndecide (an < bn) = truea < b
    theorem Mathlib.Meta.NormNum.isNat_ordinalLT_false {a b : Ordinal.{u}} {an bn : } :
    IsNat a anIsNat b bndecide (an < bn) = false¬a < b

    The norm_num extension for inequality on ordinals.

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

      The norm_num extension for strict inequality on ordinals.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem Mathlib.Meta.NormNum.isNat_ordinalSub {a b : Ordinal.{u}} {an bn rn : } :
        IsNat a anIsNat b bnan - bn = rnIsNat (a - b) rn

        The norm_num extension for subtration on ordinals.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem Mathlib.Meta.NormNum.isNat_ordinalDiv {a b : Ordinal.{u}} {an bn rn : } :
          IsNat a anIsNat b bnan / bn = rnIsNat (a / b) rn

          The norm_num extension for division on ordinals.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem Mathlib.Meta.NormNum.isNat_ordinalMod {a b : Ordinal.{u}} {an bn rn : } :
            IsNat a anIsNat b bnan % bn = rnIsNat (a % b) rn

            The norm_num extension for modulo on ordinals.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem Mathlib.Meta.NormNum.isNat_ordinalOPow {a b : Ordinal.{u}} {an bn rn : } :
              IsNat a anIsNat b bnan ^ bn = rnIsNat (a ^ b) rn

              The norm_num extension for homogenous power on ordinals.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem Mathlib.Meta.NormNum.isNat_ordinalNPow {a : Ordinal.{u}} {b an bn rn : } :
                IsNat a anIsNat b bnan ^ bn = rnIsNat (a ^ b) rn

                The norm_num extension for natural power on ordinals.

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