PeanoMinus

@[implicit_reducible]

def LO.Arith.instLEofPeanoMinus {M : Type u_1} [ORingStruc M] : LE M

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.instLEofPeanoMinus = { le := fun (x y : M) => x = y ∨ x < y }

theorem LO.Arith.le_def {M : Type u_1} [ORingStruc M] {x y : M} : x ≤ y ↔ x = y ∨ x < y

theorem LO.Arith.add_zero {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) : x + 0 = x

theorem LO.Arith.add_assoc {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x y z : M) : x + y + z = x + (y + z)

theorem LO.Arith.add_comm {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x y : M) : x + y = y + x

theorem LO.Arith.add_eq_of_lt {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x y : M) : x < y → ∃ (z : M), x + z = y

@[simp]

theorem LO.Arith.zero_le {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) : 0 ≤ x

theorem LO.Arith.zero_lt_one {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] : 0 < 1

theorem LO.Arith.one_le_of_zero_lt {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) : 0 < x → 1 ≤ x

theorem LO.Arith.add_lt_add {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x y z : M) : x < y → x + z < y + z

theorem LO.Arith.mul_zero {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) : x * 0 = 0

theorem LO.Arith.mul_one {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) : x * 1 = x

theorem LO.Arith.mul_assoc {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x y z : M) : x * y * z = x * (y * z)

theorem LO.Arith.mul_comm {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x y : M) : x * y = y * x

theorem LO.Arith.mul_lt_mul {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x y z : M) : x < y → 0 < z → x * z < y * z

theorem LO.Arith.distr {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x y z : M) : x * (y + z) = x * y + x * z

theorem LO.Arith.lt_irrefl {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) : ¬x < x

theorem LO.Arith.lt_trans {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x y z : M) : x < y → y < z → x < z

theorem LO.Arith.lt_tri {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x y : M) : x < y ∨ x = y ∨ y < x

@[implicit_reducible]

def LO.Arith.instAddCommMonoidOfPeanoMinus {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] : AddCommMonoid M

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

def LO.Arith.instCommMonoidOfPeanoMinus {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] : CommMonoid M

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

noncomputable def LO.Arith.instLinearOrderOfPeanoMinus {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] : LinearOrder M

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.zero_mul {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) : 0 * x = 0

@[implicit_reducible]

def LO.Arith.instCommSemiringOfPeanoMinus {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] : CommSemiring M

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.instIsOrderedCancelAddMonoid_leanPool {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] : IsOrderedCancelAddMonoid M

theorem LO.Arith.instZeroLEOneClass_leanPool {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] : ZeroLEOneClass M

theorem LO.Arith.instNontrivial_leanPool {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] : Nontrivial M

theorem LO.Arith.instPosMulStrictMono_leanPool {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] : PosMulStrictMono M

theorem LO.Arith.instMulPosStrictMono_leanPool {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] : MulPosStrictMono M

theorem LO.Arith.instIsStrictOrderedRing_leanPool {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] : IsStrictOrderedRing M

theorem LO.Arith.instCanonicallyOrderedAdd_leanPool {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] : CanonicallyOrderedAdd M

theorem LO.Arith.numeral_eq_natCast {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (n : ℕ) : ORingStruc.numeral n = ↑n

theorem LO.Arith.not_neg {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) : ¬x < 0

theorem LO.Arith.eq_succ_of_pos {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {x : M} (h : 0 < x) : ∃ (y : M), x = y + 1

theorem LO.Arith.le_iff_lt_succ {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {x y : M} : x ≤ y ↔ x < y + 1

theorem LO.Arith.eq_nat_of_lt_nat {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {n : ℕ} {x : M} : x < ↑n → ∃ (m : ℕ), x = ↑m

instance LO.Arith.qq {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] : M ⊧ₘ* 𝐑₀

instance LO.FirstOrder.Arith.instWeakerThanSyntacticFormulaORingTheoryCobhamR0PeanoMinus : 𝐑₀ wkn 𝐏𝐀⁻

instance LO.FirstOrder.Arith.instStrictlyWeakerThanSyntacticFormulaORingTheoryCobhamR0PeanoMinus : 𝐑₀ swkn 𝐏𝐀⁻