Documentation

CombinatorialGames.Nimber.SimplestExtension.Closure

Closures #

We define groupClosure, ringClosure, and fieldClosure, which represent the smallest nimber equal or greater to another, which satisfies IsGroup, IsRing, or IsField.

For Mathlib #

source
@[simp]
theorem Subring.coe_eq_univ {R : Type u_1} [Ring R] {H : Subring R} :
↑H = Set.univ ↔ H = ⊤
source
@[simp]
theorem Subfield.coe_eq_univ {R : Type u_1} [Field R] {H : Subfield R} :
↑H = Set.univ ↔ H = ⊤
source
@[simp]
theorem Subfield.toSubring_eq_top {R : Type u_1} [Field R] {H : Subfield R} :
H.toSubring = ⊤ ↔ H = ⊤
source
@[simp]
theorem Subfield.coe_bot {R : Type u_1} [DivisionRing R] :
↑⊥ = Set.range Rat.cast
source
instance Subfield.small_closure {R : Type u_1} (s : Set R) [DivisionRing R] [Small.{u, u_1} ↑s] :
Small.{u, u_1} ↥(closure s)
source
instance Subfield.small_closure' {R : Type u_1} (s : Set R) [DivisionRing R] [Small.{u, u_1} ↑s] :
Small.{u, u_1} ↑↑(closure s)

Groups #

source
theorem Nimber.isGroup_sInf_compl (s : AddSubgroup Nimber) (hs : s ≠ ⊤) :
(sInf (↑s)ᶜ).IsGroup
source
theorem Nimber.isLowerSet_addSubgroupClosure {s : Set Nimber} (hs : IsLowerSet s) :
IsLowerSet ↑(AddSubgroup.closure s)
source
instance Nimber.small_addSubgroupClosure (s : Set Nimber) [Small.{u, u_1 + 1} ↑s] :
Small.{u, u_1 + 1} ↥(AddSubgroup.closure s)
source
theorem Nimber.addSubgroupClosure_Iio_eq_Iio (x : Nimber) :
∃ (y : Nimber), ↑(AddSubgroup.closure (Set.Iio x)) = Set.Iio y
source
noncomputable def Nimber.groupClosure (x : Nimber) :
Nimber

Returns the smallest IsGroup that's at least x.

Equations
Instances For
    source
    @[simp]
    theorem Nimber.coe_addSubgroupClosure_Iio (x : Nimber) :
    ↑(AddSubgroup.closure (Set.Iio x)) = Set.Iio x.groupClosure
    source
    @[simp]
    theorem Nimber.mem_addSubgroupClosure_Iio {x y : Nimber} :
    y ∈ AddSubgroup.closure (Set.Iio x) ↔ y < x.groupClosure
    source
    @[simp]
    theorem Nimber.le_groupClosure (x : Nimber) :
    x ≤ x.groupClosure
    source
    @[simp]
    theorem Nimber.IsGroup.groupClosure (x : Nimber) :
    x.groupClosure.IsGroup
    source
    theorem Nimber.IsGroup.groupClosure_le_iff {x y : Nimber} (h : x.IsGroup) :
    y.groupClosure ≤ x ↔ y ≤ x
    source
    theorem Nimber.IsGroup.lt_groupClosure_iff {x y : Nimber} (h : x.IsGroup) :
    x < y.groupClosure ↔ x < y
    source
    theorem Nimber.IsGroup.groupClosure_eq {x : Nimber} (h : x.IsGroup) :
    x.groupClosure = x
    source
    theorem Nimber.groupClosure_mono :
    Monotone groupClosure
    source
    @[simp]
    theorem Nimber.groupClosure_zero :
    groupClosure 0 = 1
    source
    @[simp]
    theorem Nimber.groupClosure_one :
    groupClosure 1 = 1
    source
    @[simp]
    theorem Nimber.groupClosure_two :
    (of 2).groupClosure = of 2
    source
    @[simp]
    theorem Nimber.groupClosure.two_opow (x : Ordinal.{u_1}) :
    (of (2 ^ x)).groupClosure = of (2 ^ x)
    source
    theorem Nimber.groupClosure_of_not_isGroup {x : Nimber} (h : ¬x.IsGroup) (hx₀ : x ≠ 0) :
    x.groupClosure = of (2 ^ (Ordinal.log 2 (val x) + 1))

    Rings #

    source
    theorem Nimber.isRing_sInf_compl (s : Subring Nimber) (hs : s ≠ ⊤) :
    (sInf (↑s)ᶜ).IsRing
    source
    theorem Nimber.isLowerSet_subringClosure {s : Set Nimber} (hs : IsLowerSet s) :
    IsLowerSet ↑(Subring.closure s)
    source
    instance Nimber.small_subringClosure (s : Set Nimber) [Small.{u, u_1 + 1} ↑s] :
    Small.{u, u_1 + 1} ↥(Subring.closure s)
    source
    theorem Nimber.subringClosure_Iio_eq_Iio (x : Nimber) :
    ∃ (y : Nimber), ↑(Subring.closure (Set.Iio x)) = Set.Iio y
    source
    noncomputable def Nimber.ringClosure (x : Nimber) :
    Nimber

    Returns the smallest IsRing that's at least x.

    Equations
    Instances For
      source
      @[simp]
      theorem Nimber.coe_subringClosure_Iio (x : Nimber) :
      ↑(Subring.closure (Set.Iio x)) = Set.Iio x.ringClosure
      source
      @[simp]
      theorem Nimber.mem_subringClosure_Iio {x y : Nimber} :
      y ∈ Subring.closure (Set.Iio x) ↔ y < x.ringClosure
      source
      @[simp]
      theorem Nimber.le_ringClosure (x : Nimber) :
      x ≤ x.ringClosure
      source
      @[simp]
      theorem Nimber.IsRing.ringClosure (x : Nimber) :
      x.ringClosure.IsRing
      source
      theorem Nimber.IsRing.ringClosure_le_iff {x y : Nimber} (h : x.IsRing) :
      y.ringClosure ≤ x ↔ y ≤ x
      source
      theorem Nimber.IsRing.lt_ringClosure_iff {x y : Nimber} (h : x.IsRing) :
      x < y.ringClosure ↔ x < y
      source
      theorem Nimber.IsRing.ringClosure_eq {x : Nimber} (h : x.IsRing) :
      x.ringClosure = x
      source
      theorem Nimber.ringClosure_mono :
      Monotone ringClosure
      source
      @[simp]
      theorem Nimber.ringClosure_zero :
      ringClosure 0 = of 2
      source
      @[simp]
      theorem Nimber.ringClosure_one :
      ringClosure 1 = of 2
      source
      @[simp]
      theorem Nimber.ringClosure_two :
      (of 2).ringClosure = of 2
      source
      theorem Nimber.groupClosure_le_ringClosure (x : Nimber) :
      x.groupClosure ≤ x.ringClosure

      Fields #

      source
      theorem Nimber.isField_sInf_compl (s : Subfield Nimber) (hs : s ≠ ⊤) :
      (sInf (↑s)ᶜ).IsField
      source
      theorem Nimber.isLowerSet_subfieldClosure {s : Set Nimber} (hs : IsLowerSet s) :
      IsLowerSet ↑(Subfield.closure s)
      source
      instance Nimber.small_subfieldClosure (s : Set Nimber) [Small.{u, u_1 + 1} ↑s] :
      Small.{u, u_1 + 1} ↥(Subfield.closure s)
      source
      theorem Nimber.subfieldClosure_Iio_eq_Iio (x : Nimber) :
      ∃ (y : Nimber), ↑(Subfield.closure (Set.Iio x)) = Set.Iio y
      source
      noncomputable def Nimber.fieldClosure (x : Nimber) :
      Nimber

      Returns the smallest IsField that's at least x.

      Equations
      Instances For
        source
        @[simp]
        theorem Nimber.coe_subfieldClosure_Iio (x : Nimber) :
        ↑(Subfield.closure (Set.Iio x)) = Set.Iio x.fieldClosure
        source
        @[simp]
        theorem Nimber.mem_subfieldClosure_Iio {x y : Nimber} :
        y ∈ Subfield.closure (Set.Iio x) ↔ y < x.fieldClosure
        source
        @[simp]
        theorem Nimber.le_fieldClosure (x : Nimber) :
        x ≤ x.fieldClosure
        source
        @[simp]
        theorem Nimber.IsField.fieldClosure (x : Nimber) :
        x.fieldClosure.IsField
        source
        theorem Nimber.IsField.fieldClosure_le_iff {x y : Nimber} (h : x.IsField) :
        y.fieldClosure ≤ x ↔ y ≤ x
        source
        theorem Nimber.IsField.lt_fieldClosure_iff {x y : Nimber} (h : x.IsField) :
        x < y.fieldClosure ↔ x < y
        source
        theorem Nimber.IsField.fieldClosure_eq {x : Nimber} (h : x.IsField) :
        x.fieldClosure = x
        source
        theorem Nimber.fieldClosure_mono :
        Monotone fieldClosure
        source
        @[simp]
        theorem Nimber.fieldClosure_zero :
        fieldClosure 0 = of 2
        source
        @[simp]
        theorem Nimber.fieldClosure_one :
        fieldClosure 1 = of 2
        source
        @[simp]
        theorem Nimber.fieldClosure_two :
        (of 2).fieldClosure = of 2
        source
        theorem Nimber.ringClosure_le_fieldClosure (x : Nimber) :
        x.ringClosure ≤ x.fieldClosure
        source
        theorem Nimber.groupClosure_le_fieldClosure (x : Nimber) :
        x.groupClosure ≤ x.fieldClosure