Documentation

CombinatorialGames.Nimber.Nat

Finite nimber arithmetic #

This file defines the type alias NatNimber of the natural numbers, endowed with nimber arithmetic. The goal is to define the field structure computably, and prove that it matches that on Nimber.

source
@[implicit_reducible]
instance instOneNatNimber :
One NatNimber
Equations
source
theorem NatNimber.pos_iff_ne_zero {a✝ : NatNimber} :
0 < a✝ ↔ a✝ ≠ 0
source
@[simp]
theorem NatNimber.of_eq_zero {a✝ : ℕ} :
of a✝ = 0 ↔ a✝ = 0
source
@[implicit_reducible]
instance NatNimber.instOrderBot :
OrderBot NatNimber
Equations
source
theorem NatNimber.of_ne_one {a✝ : ℕ} :
of a✝ ≠ 1 ↔ a✝ ≠ 1
source
theorem NatNimber.induction {p✝ : NatNimber → Prop} (i✝ : NatNimber) :
(∀ (j : NatNimber), (∀ k < j, p✝ k) → p✝ j) → p✝ i✝

Well-founded induction for NatNimber.

source
@[simp]
theorem NatNimber.of_eq_one {a✝ : ℕ} :
of a✝ = 1 ↔ a✝ = 1
source
@[implicit_reducible]
noncomputable instance NatNimber.instConditionallyCompleteLinearOrderBot :
ConditionallyCompleteLinearOrderBot NatNimber
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem NatNimber.val_eq_zero {a✝ : NatNimber} :
val a✝ = 0 ↔ a✝ = 0
source
theorem NatNimber.eq_zero_or_pos (a✝ : NatNimber) :
a✝ = 0 ∨ 0 < a✝
source
theorem NatNimber.val_eq_iff {a✝ : NatNimber} {b✝ : ℕ} :
val a✝ = b✝ ↔ a✝ = of b✝
source
@[simp]
theorem NatNimber.one_le_val {a✝ : NatNimber} :
1 ≤ val a✝ ↔ 1 ≤ a✝
source
@[simp]
theorem NatNimber.of_symm :
of.symm = val
source
@[simp]
theorem NatNimber.succ_of (a✝ : ℕ) :
Order.succ (of a✝) = of (a✝ + 1)
source
@[match_pattern]
def NatNimber.val :
NatNimber ≃o ℕ

The identity function between NatNimber and Nat.

Equations
Instances For
    source
    @[simp]
    theorem NatNimber.one_lt_val {a✝ : NatNimber} :
    1 < val a✝ ↔ 1 < a✝
    source
    @[implicit_reducible]
    instance instInhabitedNatNimber :
    Inhabited NatNimber
    Equations
    source
    theorem NatNimber.of_ne_zero {a✝ : ℕ} :
    of a✝ ≠ 0 ↔ a✝ ≠ 0
    source
    theorem NatNimber.val_lt_one {a✝ : NatNimber} :
    val a✝ < 1 ↔ a✝ < 1
    source
    @[implicit_reducible]
    instance NatNimber.instPartialOrder :
    PartialOrder NatNimber
    Equations
    • One or more equations did not get rendered due to their size.
    source
    theorem NatNimber.val_lt_iff {a✝ : NatNimber} {b✝ : ℕ} :
    val a✝ < b✝ ↔ a✝ < of b✝
    source
    @[simp]
    theorem NatNimber.le_zero {a✝ : NatNimber} :
    a✝ ≤ 0 ↔ a✝ = 0
    source
    @[simp]
    theorem NatNimber.one_lt_of {a✝ : ℕ} :
    1 < of a✝ ↔ 1 < a✝
    source
    @[match_pattern]
    def NatNimber.of :
    ℕ ≃o NatNimber

    The identity function between Nat and NatNimber.

    Equations
    Instances For
      source
      theorem NatNimber.succ_ne_zero (a✝ : NatNimber) :
      Order.succ a✝ ≠ 0
      source
      instance NatNimber.instZeroLEOneClass :
      ZeroLEOneClass NatNimber
      source
      @[simp]
      theorem NatNimber.of_val (a✝ : NatNimber) :
      of (val a✝) = a✝
      source
      @[simp]
      theorem NatNimber.zero_le (a✝ : NatNimber) :
      0 ≤ a✝
      source
      @[simp]
      theorem NatNimber.val_eq_one {a✝ : NatNimber} :
      val a✝ = 1 ↔ a✝ = 1
      source
      @[simp]
      theorem NatNimber.val_one :
      val 1 = 1
      source
      @[simp]
      theorem NatNimber.val_le_one {a✝ : NatNimber} :
      val a✝ ≤ 1 ↔ a✝ ≤ 1
      source
      @[simp]
      theorem NatNimber.val_symm :
      val.symm = of
      source
      @[simp]
      theorem NatNimber.not_neg (a✝ : NatNimber) :
      ¬a✝ < 0
      source
      theorem NatNimber.of_lt_iff {a✝ : ℕ} {b✝ : NatNimber} :
      of a✝ < b✝ ↔ a✝ < val b✝
      source
      theorem NatNimber.val_le_iff {a✝ : NatNimber} {b✝ : ℕ} :
      val a✝ ≤ b✝ ↔ a✝ ≤ of b✝
      source
      @[simp]
      theorem NatNimber.of_zero :
      of 0 = 0
      source
      instance NatNimber.instNoMaxOrder :
      NoMaxOrder NatNimber
      source
      theorem NatNimber.one_le_of {a✝ : ℕ} :
      1 ≤ of a✝ ↔ 1 ≤ a✝
      source
      @[implicit_reducible]
      instance instZeroNatNimber :
      Zero NatNimber
      Equations
      source
      @[simp]
      theorem NatNimber.of_le_one {a✝ : ℕ} :
      of a✝ ≤ 1 ↔ a✝ ≤ 1
      source
      @[implicit_reducible]
      instance NatNimber.instSuccOrder :
      SuccOrder NatNimber
      Equations
      • One or more equations did not get rendered due to their size.
      source
      instance NatNimber.instWellFoundedLT :
      WellFoundedLT NatNimber
      source
      @[simp]
      theorem NatNimber.of_one :
      of 1 = 1
      source
      theorem NatNimber.val_ne_zero {a✝ : NatNimber} :
      val a✝ ≠ 0 ↔ a✝ ≠ 0
      source
      @[implicit_reducible]
      instance instWellFoundedRelationNatNimber :
      WellFoundedRelation NatNimber
      Equations
      source
      instance NatNimber.instNeZeroOfNat :
      NeZero 1
      source
      @[simp]
      theorem NatNimber.bot_eq_zero :
      ⊥ = 0
      source
      @[simp]
      theorem NatNimber.val_zero :
      val 0 = 0
      source
      theorem NatNimber.val_ne_one {a✝ : NatNimber} :
      val a✝ ≠ 1 ↔ a✝ ≠ 1
      source
      @[implicit_reducible]
      instance instNontrivialNatNimber :
      Nontrivial NatNimber
      Equations
      source
      theorem NatNimber.of_lt_one {a✝ : ℕ} :
      of a✝ < 1 ↔ a✝ < 1
      source
      theorem NatNimber.of_eq_iff {a✝ : ℕ} {b✝ : NatNimber} :
      of a✝ = b✝ ↔ a✝ = val b✝
      source
      @[simp]
      theorem NatNimber.val_of (a✝ : ℕ) :
      val (of a✝) = a✝
      source
      theorem NatNimber.lt_wf :
      WellFounded fun (x1 x2 : NatNimber) => x1 < x2
      source
      theorem NatNimber.succ_def (a✝ : NatNimber) :
      Order.succ a✝ = of (val a✝ + 1)
      source
      theorem NatNimber.of_le_iff {a✝ : ℕ} {b✝ : NatNimber} :
      of a✝ ≤ b✝ ↔ a✝ ≤ val b✝
      source
      def NatNimber.ind {motive✝ : NatNimber → Sort u_1} (of : (a : ℕ) → motive✝ (of a)) (a✝ : NatNimber) :
      motive✝ a✝

      A recursor for NatNimber. Use as cases x.

      Equations
      Instances For
        source
        def NatNimber :
        Type

        The natural numbers, endowed with nim operations.

        Equations
        Instances For