Documentation

Arithmetization.Basic.PeanoMinus

theorem LO.Arith.sub_existsUnique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (a : V) (b : V) :
∃! c : V, (a ba = b + c) (a < bc = 0)
def LO.Arith.sub {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (a : V) (b : V) :
V
Equations
Instances For
    Equations
    • LO.Arith.instSub_arithmetization = { sub := LO.Arith.sub }
    theorem LO.Arith.sub_spec_of_ge {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} (h : a b) :
    a = b + (a - b)
    theorem LO.Arith.sub_spec_of_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} (h : a < b) :
    a - b = 0
    theorem LO.Arith.sub_eq_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} {c : V} :
    c = a - b (a ba = b + c) (a < bc = 0)
    @[simp]
    theorem LO.Arith.sub_le_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (a : V) (b : V) :
    a - b a
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      instance LO.Arith.sub_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) :
      -Function₂ fun (x x_1 : V) => x - x_1
      Equations
      • =
      Equations
      • =
      @[simp]
      theorem LO.Arith.sub_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (a : V) :
      a - a = 0
      theorem LO.Arith.sub_spec_of_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} (h : a b) :
      a - b = 0
      theorem LO.Arith.sub_add_self_of_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} (h : b a) :
      a - b + b = a
      theorem LO.Arith.add_tsub_self_of_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} (h : b a) :
      b + (a - b) = a
      @[simp]
      theorem LO.Arith.add_sub_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} :
      a + b - b = a
      @[simp]
      theorem LO.Arith.add_sub_self' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} :
      b + a - b = a
      @[simp]
      theorem LO.Arith.zero_sub {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (a : V) :
      0 - a = 0
      @[simp]
      theorem LO.Arith.sub_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (a : V) :
      a - 0 = a
      theorem LO.Arith.sub_remove_left {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} {c : V} (e : a = b + c) :
      a - c = b
      theorem LO.Arith.sub_sub {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} {c : V} :
      a - b - c = a - (b + c)
      @[simp]
      theorem LO.Arith.pos_sub_iff_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} :
      0 < a - b b < a
      @[simp]
      theorem LO.Arith.sub_eq_zero_iff_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} :
      a - b = 0 a b
      theorem LO.Arith.zero_or_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (a : V) :
      a = 0 ∃ (a' : V), a = a' + 1
      theorem LO.Arith.pred_lt_self_of_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} (h : 0 < a) :
      a - 1 < a
      theorem LO.Arith.tsub_lt_iff_left {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} {c : V} (h : b a) :
      a - b < c a < c + b
      theorem LO.Arith.sub_mul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} {c : V} (h : b a) :
      (a - b) * c = a * c - b * c
      theorem LO.Arith.mul_sub {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} {c : V} (h : b a) :
      c * (a - b) = c * a - c * b
      theorem LO.Arith.add_sub_of_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {b : V} {c : V} (h : c b) (a : V) :
      a + b - c = a + (b - c)
      theorem LO.Arith.sub_succ_add_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {x : V} {y : V} (h : y < x) (z : V) :
      x - (y + 1) + (z + 1) = x - y + z
      theorem LO.Arith.le_sub_one_of_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} (h : a < b) :
      a b - 1
      theorem LO.Arith.le_mul_self_of_pos_left {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} (hy : 0 < b) :
      a b * a
      theorem LO.Arith.le_mul_self_of_pos_right {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} (hy : 0 < b) :
      a a * b
      theorem LO.Arith.dvd_iff_bounded {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} :
      a b cb, b = a * c
      def LO.FirstOrder.Arith.dvd :
      𝚺₀.Semisentence 2
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        instance LO.Arith.dvd_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) :
        -Relation fun (x x_1 : V) => x x_1
        Equations
        • =
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem LO.Arith.le_of_dvd {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} (h : 0 < b) :
          a ba b
          theorem LO.Arith.not_dvd_of_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} (pos : 0 < b) :
          b < a¬a b
          theorem LO.Arith.dvd_antisymm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} :
          a bb aa = b
          theorem LO.Arith.dvd_one_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} :
          a 1 a = 1
          theorem LO.Arith.units_eq_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (u : Vˣ) :
          u = 1
          @[simp]
          theorem LO.Arith.unit_iff_eq_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} :
          IsUnit a a = 1
          theorem LO.Arith.eq_one_or_eq_of_dvd_of_prime {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {p : V} {a : V} (pp : Prime p) (hxp : a p) :
          a = 1 a = p
          Equations
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def LO.FirstOrder.Arith.min :
              𝚺₀.Semisentence 3
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def LO.FirstOrder.Arith.max :
                𝚺₀.Semisentence 3
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For