ZFC Integers

This file provides a construction of the integers in ZFC based on the construction of natural numbers. It follows the usual construction of integers as equivalence classes of pairs of natural numbers.

The theory also comes with usual theorems and arithmetic operations on integers and wraps everything in a commutative ring structure.

Finally, we show that the ZFInt type is in canonical bijection with the type of elements contained in ZFSet.Int. The bijection is built directly from the projection functions ZFInt.into and ZFInt.outof — no Schröder–Bernstein, no Classical.choice over a non-empty set of bijections — so the induced order on {x // x ∈ ZFSet.Int} is well-defined and concrete inequalities like 0 < 1 are provable.

@[reducible, inline]

abbrev ZFSet.zrel (a b : ZFNat × ZFNat) : Prop

Equations

• ZFSet.zrel a b = (a.1 + b.2 = a.2 + b.1)

def ZFSet.zrel_eq : Equivalence ZFSet.zrel

Equations

• ZFSet.zrel_eq = ⋯

@[implicit_reducible]

instance ZFSet.instSetoidZFNatZFNat : Setoid (ZFNat × ZFNat)

Equations

• ZFSet.instSetoidZFNatZFNat = { r := ZFSet.zrel, iseqv := ZFSet.zrel_eq }

@[reducible, inline]

abbrev ZFSet.ZFInt : Type (u_1 + 1)

Equations

• ZFSet.ZFInt = Quotient ZFSet.instSetoidZFNatZFNat

def ZFSet.ZFInt.mk : ZFNat × ZFNat → ZFInt

Equations

• ZFSet.ZFInt.mk = Quotient.mk''

@[simp]

theorem ZFSet.ZFInt.mk_eq (x : ZFNat × ZFNat) : ⟦x⟧ = mk x

@[simp]

theorem ZFSet.ZFInt.mk_out (x : ZFInt) : mk (Quotient.out x) = x

theorem ZFSet.ZFInt.eq {x y : ZFNat × ZFNat} : mk x = mk y ↔ ZFSet.zrel x y

theorem ZFSet.ZFInt.sound {x y : ZFNat × ZFNat} (h : ZFSet.zrel x y) : mk x = mk y

theorem ZFSet.ZFInt.exact {x y : ZFNat × ZFNat} : mk x = mk y → ZFSet.zrel x y

@[reducible, inline]

abbrev ZFSet.ZFInt.zero : ZFInt

Equations

• ZFSet.ZFInt.zero = ZFSet.ZFInt.mk (0, 0)

@[reducible, inline]

abbrev ZFSet.ZFInt.one : ZFInt

Equations

• ZFSet.ZFInt.one = ZFSet.ZFInt.mk (1, 0)

@[implicit_reducible]

instance ZFSet.ZFInt.instZero : Zero ZFInt

Equations

• ZFSet.ZFInt.instZero = { zero := ZFSet.ZFInt.zero }

@[implicit_reducible]

instance ZFSet.ZFInt.instOne : One ZFInt

Equations

• ZFSet.ZFInt.instOne = { one := ZFSet.ZFInt.one }

theorem ZFSet.ZFInt.zero_eq : 0 = mk (0, 0)

theorem ZFSet.ZFInt.one_eq : 1 = mk (1, 0)

theorem ZFSet.ZFInt.one_ne_zero : 1 ≠ 0

theorem ZFSet.ZFInt.mk_eq_zero_iff {n m : ZFNat} : mk (n, m) = 0 ↔ n = m

@[reducible, inline]

noncomputable abbrev ZFSet.ZFInt.add (n m : ZFInt) : ZFInt

Equations

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

@[implicit_reducible]

noncomputable instance ZFSet.ZFInt.instAdd : Add ZFInt

Equations

• ZFSet.ZFInt.instAdd = { add := ZFSet.ZFInt.add }

theorem ZFSet.ZFInt.add_eq (n m : ZFNat × ZFNat) : mk n + mk m = mk (n.1 + m.1, n.2 + m.2)

theorem ZFSet.ZFInt.add_assoc (n m k : ZFInt) : n + (m + k) = n + m + k

theorem ZFSet.ZFInt.add_comm (n m : ZFInt) : n + m = m + n

theorem ZFSet.ZFInt.add_left_comm (n m k : ZFInt) : n + (m + k) = m + (n + k)

theorem ZFSet.ZFInt.add_right_comm (n m k : ZFInt) : n + m + k = n + k + m

@[simp]

theorem ZFSet.ZFInt.add_zero {x : ZFInt} : x + 0 = x

@[simp]

theorem ZFSet.ZFInt.zero_add {x : ZFInt} : 0 + x = x

@[reducible, inline]

abbrev ZFSet.ZFInt.neg (n : ZFInt) : ZFInt

Equations

• n.neg = Quotient.liftOn n (fun (x : ZFSet.ZFNat × ZFSet.ZFNat) => ZFSet.ZFInt.mk (x.2, x.1)) ZFSet.ZFInt.neg._proof_1

@[implicit_reducible]

instance ZFSet.ZFInt.instNeg : Neg ZFInt

Equations

• ZFSet.ZFInt.instNeg = { neg := ZFSet.ZFInt.neg }

theorem ZFSet.ZFInt.neg_eq (n : ZFNat × ZFNat) : -mk n = mk (n.2, n.1)

@[simp]

theorem ZFSet.ZFInt.neg_neg (n : ZFInt) : - -n = n

@[simp]

theorem ZFSet.ZFInt.neg_zero : -0 = 0

theorem ZFSet.ZFInt.neg_inj {a b : ZFInt} : -a = -b ↔ a = b

@[simp]

theorem ZFSet.ZFInt.neg_eq_zero {a : ZFInt} : -a = 0 ↔ a = 0

theorem ZFSet.ZFInt.neg_ne_zero {a : ZFInt} : -a ≠ 0 ↔ a ≠ 0

theorem ZFSet.ZFInt.add_left_neg {a : ZFInt} : -a + a = 0

theorem ZFSet.ZFInt.add_right_neg (a : ZFInt) : a + -a = 0

theorem ZFSet.ZFInt.neg_eq_of_add_eq_zero {a b : ZFInt} (h : a + b = 0) : -a = b

theorem ZFSet.ZFInt.eq_neg_of_eq_neg {a b : ZFInt} (h : a = -b) : b = -a

theorem ZFSet.ZFInt.eq_neg_comm {a b : ZFInt} : a = -b ↔ b = -a

theorem ZFSet.ZFInt.neg_eq_comm {a b : ZFInt} : -a = b ↔ -b = a

theorem ZFSet.ZFInt.neg_add_cancel_left (a b : ZFInt) : -a + (a + b) = b

theorem ZFSet.ZFInt.add_neg_cancel_left (a b : ZFInt) : a + (-a + b) = b

theorem ZFSet.ZFInt.add_neg_cancel_right (a b : ZFInt) : a + b + -b = a

theorem ZFSet.ZFInt.neg_add_cancel_right (a b : ZFInt) : a + -b + b = a

theorem ZFSet.ZFInt.add_left_cancel {a b c : ZFInt} (h : a + b = a + c) : b = c

@[simp]

theorem ZFSet.ZFInt.neg_add {a b : ZFInt} : -(a + b) = -a + -b

@[reducible, inline]

noncomputable abbrev ZFSet.ZFInt.sub (n m : ZFInt) : ZFInt

Equations

• n.sub m = n + -m

@[implicit_reducible]

noncomputable instance ZFSet.ZFInt.instSub : Sub ZFInt

Equations

• ZFSet.ZFInt.instSub = { sub := ZFSet.ZFInt.sub }

theorem ZFSet.ZFInt.sub_eq (n m : ZFNat × ZFNat) : mk n - mk m = mk (n.1 + m.2, n.2 + m.1)

theorem ZFSet.ZFInt.sub_eq_add_neg {a b : ZFInt} : a - b = a + -b

theorem ZFSet.ZFInt.add_neg_one (i : ZFInt) : i + -1 = i - 1

@[simp]

theorem ZFSet.ZFInt.sub_self (a : ZFInt) : a - a = 0

@[simp]

theorem ZFSet.ZFInt.sub_zero (a : ZFInt) : a - 0 = a

@[simp]

theorem ZFSet.ZFInt.zero_sub (a : ZFInt) : 0 - a = -a

theorem ZFSet.ZFInt.sub_eq_zero_of_eq {a b : ZFInt} (h : a = b) : a - b = 0

theorem ZFSet.ZFInt.eq_of_sub_eq_zero {a b : ZFInt} (h : a - b = 0) : a = b

theorem ZFSet.ZFInt.sub_eq_zero {a b : ZFInt} : a - b = 0 ↔ a = b

theorem ZFSet.ZFInt.sub_sub (a b c : ZFInt) : a - b - c = a - (b + c)

theorem ZFSet.ZFInt.neg_sub (a b : ZFInt) : -(a - b) = b - a

theorem ZFSet.ZFInt.sub_sub_self (a b : ZFInt) : a - (a - b) = b

@[simp]

theorem ZFSet.ZFInt.sub_neg (a b : ZFInt) : a - -b = a + b

@[simp]

theorem ZFSet.ZFInt.sub_add_cancel (a b : ZFInt) : a - b + b = a

@[simp]

theorem ZFSet.ZFInt.add_sub_cancel (a b : ZFInt) : a + b - b = a

theorem ZFSet.ZFInt.add_sub_assoc (a b c : ZFInt) : a + b - c = a + (b - c)

theorem ZFSet.ZFInt.sub_left_cancel (a b c : ZFInt) : a - c = b - c → a = b

theorem ZFSet.ZFInt.sub_right_cancel (a b c : ZFInt) : c - a = c - b → a = b

theorem ZFSet.ZFInt.add_eq_sub_iff {a b c : ZFInt} : a + b = c ↔ a = c - b

@[reducible, inline]

noncomputable abbrev ZFSet.ZFInt.nsmul : ℕ → ZFInt → ZFInt

Equations

• ZFSet.ZFInt.nsmul 0 x✝ = 0
• ZFSet.ZFInt.nsmul n.succ x✝ = x✝ + ZFSet.ZFInt.nsmul n x✝

@[reducible, inline]

noncomputable abbrev ZFSet.ZFInt.zsmul (n : ℤ) (x : ZFInt) : ZFInt

Equations

• ZFSet.ZFInt.zsmul (Int.ofNat n_2) x = ZFSet.ZFInt.nsmul n_2 x
• ZFSet.ZFInt.zsmul (Int.negSucc n_2) x = -ZFSet.ZFInt.nsmul (n_2 + 1) x

theorem ZFSet.ZFInt.mul_wf {a b c d s t u v : ZFNat} (h₁ : ZFSet.zrel (a, b) (s, t)) (h₂ : ZFSet.zrel (c, d) (u, v)) : ZFSet.zrel (a * c + b * d, a * d + b * c) (s * u + t * v, s * v + t * u)

@[reducible, inline]

noncomputable abbrev ZFSet.ZFInt.mul (n m : ZFInt) : ZFInt

Equations

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

@[implicit_reducible]

noncomputable instance ZFSet.ZFInt.instMul : Mul ZFInt

Equations

• ZFSet.ZFInt.instMul = { mul := ZFSet.ZFInt.mul }

theorem ZFSet.ZFInt.mul_eq (n m : ZFNat × ZFNat) : mk n * mk m = mk (n.1 * m.1 + n.2 * m.2, n.1 * m.2 + n.2 * m.1)

theorem ZFSet.ZFInt.mul_comm (n m : ZFInt) : n * m = m * n

theorem ZFSet.ZFInt.left_distrib (a b c : ZFInt) : a * (b + c) = a * b + a * c

theorem ZFSet.ZFInt.right_distrib (a b c : ZFInt) : (a + b) * c = a * c + b * c

@[simp]

theorem ZFSet.ZFInt.zero_mul (a : ZFInt) : 0 * a = 0

@[simp]

theorem ZFSet.ZFInt.mul_zero (a : ZFInt) : a * 0 = 0

theorem ZFSet.ZFInt.mul_assoc (a b c : ZFInt) : a * b * c = a * (b * c)

@[simp]

theorem ZFSet.ZFInt.one_mul (a : ZFInt) : 1 * a = a

@[simp]

theorem ZFSet.ZFInt.mul_one (a : ZFInt) : a * 1 = a

@[implicit_reducible]

noncomputable instance ZFSet.ZFInt.instCommRing : CommRing ZFInt

Equations

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

@[implicit_reducible]

instance ZFSet.ZFInt.int_lt : LT ZFInt

Equations

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

@[implicit_reducible]

instance ZFSet.ZFInt.int_le : LE ZFInt

Equations

• ZFSet.ZFInt.int_le = { le := fun (x y : ZFSet.ZFInt) => x < y ∨ x = y }

theorem ZFSet.ZFInt.lt_succ {n : ZFInt} : n < n + 1

theorem ZFSet.ZFInt.lt_trans {a b c : ZFInt} : a < b → b < c → a < c

theorem ZFSet.ZFInt.lt_irrefl {a : ZFInt} : ¬a < a

theorem ZFSet.ZFInt.lt_zero_iff {n m : ZFNat} : m < n ↔ 0 < mk (n, m)

theorem ZFSet.ZFInt.neg_one_lt_zero : -1 < 0

theorem ZFSet.ZFInt.zero_lt_one : 0 < 1

theorem ZFSet.ZFInt.le_trans {a b c : ZFInt} : a ≤ b → b ≤ c → a ≤ c

theorem ZFSet.ZFInt.le_antisymm {a b : ZFInt} : a ≤ b → b ≤ a → a = b

theorem ZFSet.ZFInt.le_total {a b : ZFInt} : a ≤ b ∨ b ≤ a

theorem ZFSet.ZFInt.lt_iff_le_not_ge {x y : ZFInt} : x < y ↔ x ≤ y ∧ ¬y ≤ x

theorem ZFSet.ZFInt.lt_neg_iff {a b : ZFInt} : a < b ↔ -b < -a

theorem ZFSet.ZFInt.le_neg_iff {a b : ZFInt} : a ≤ b ↔ -b ≤ -a

@[implicit_reducible]

noncomputable instance ZFSet.ZFInt.instLinearOrder : LinearOrder ZFInt

Equations

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

@[implicit_reducible]

noncomputable instance ZFSet.ZFInt.instAddCommGroup : AddCommGroup ZFInt

Equations

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

@[implicit_reducible]

instance ZFSet.ZFInt.instPartialOrder : PartialOrder ZFInt

Equations

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

instance ZFSet.ZFInt.instIsOrderedAddMonoid : IsOrderedAddMonoid ZFInt

theorem ZFSet.ZFInt.ind {P : ZFNat → ZFNat → Prop} (n : ZFNat) (m : ZFNat) (zero : P 0 0) (succ_l : ∀ (n : ZFNat) (m : ZFNat), P n m → P (n + 1) m) (succ_r : ∀ (n : ZFNat) (m : ZFNat), P n m → P n (m + 1)) : P n m

theorem ZFSet.ZFInt.induction_pos {P : ZFInt → Prop} (n : ZFInt) (n_pos : 0 ≤ n) (zero : P 0) (succ : ∀ (k : ZFInt), P k → P (k + 1)) : P n

theorem ZFSet.ZFInt.induction_neg {P : ZFInt → Prop} (n : ZFInt) (n_neg : n ≤ 0) (zero : P 0) (succ : ∀ (k : ZFInt), P k → P (k - 1)) : P n

theorem ZFSet.ZFInt.induction {P : ZFInt → Prop} (n : ZFInt) (zero : P 0) (pos : ∀ (k : ZFInt), P k → P (k + 1)) (neg : ∀ (k : ZFInt), P k → P (k - 1)) : P n

theorem ZFSet.ZFInt.sign_cases {P : ZFInt → Prop} (n : ZFInt) (zero : P 0) (neg : n < 0 → P n) (pos : 0 < n → P n) : P n

theorem ZFSet.ZFInt.cases {P : ZFInt → Prop} (n : ZFInt) (pos : 0 ≤ n → P n) (neg : n < 0 → P n) : P n

theorem ZFSet.ZFInt.add_eq_add_sub_eq_sub {a b c d : ZFNat} : a + b = c + d → a - c = d - b

theorem ZFSet.ZFInt.le_of_lt_succ (n m : ZFInt) : n < m + 1 → n ≤ m

theorem ZFSet.ZFInt.lt_succ_of_le (n m : ZFInt) : n ≤ m → n < m + 1

theorem ZFSet.ZFInt.lt_succ_of_le_iff (n m : ZFInt) : n ≤ m ↔ n < m + 1

theorem ZFSet.ZFInt.int_le.dest {n m : ZFInt} : n ≤ m → ∃ (k : ZFInt), 0 ≤ k ∧ n + k = m

theorem ZFSet.ZFInt.mul_pos_pos_pos (a b : ZFInt) (ha : 0 < a) (hb : 0 < b) : 0 < a * b

theorem ZFSet.ZFInt.neg_one_mul (a : ZFInt) : -1 * a = -a

theorem ZFSet.ZFInt.neg_one_mul_neg_one : -1 * -1 = 1

theorem ZFSet.ZFInt.mul_neg_neg (a b : ZFInt) : a * b = -a * -b

theorem ZFSet.ZFInt.neg_mul_distrib (a b : ZFInt) : -(a * b) = -a * b

theorem ZFSet.ZFInt.mul_neg_neg_pos (a b : ZFInt) (ha : a < 0) (hb : b < 0) : 0 < a * b

theorem ZFSet.ZFInt.neg_flip_lt (a : ZFInt) : a < 0 ↔ 0 < -a

theorem ZFSet.ZFInt.neg_flip_le (a : ZFInt) : a ≤ 0 ↔ 0 ≤ -a

theorem ZFSet.ZFInt.mul_neg_pos_neg (a b : ZFInt) (ha : a < 0) (hb : 0 < b) : a * b < 0

theorem ZFSet.ZFInt.mul_pos_neg_neg (a b : ZFInt) (ha : 0 < a) (hb : b < 0) : a * b < 0

theorem ZFSet.ZFInt.mul_nonneg_nonneg_nonneg (a b : ZFInt) (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b

theorem ZFSet.ZFInt.mul_nonpos_nonneg_nonpos (a b : ZFInt) (ha : a ≤ 0) (hb : 0 ≤ b) : a * b ≤ 0

theorem ZFSet.ZFInt.mul_nonneg_nonpos_nonpos (a b : ZFInt) (ha : 0 ≤ a) (hb : b ≤ 0) : a * b ≤ 0

theorem ZFSet.ZFInt.mul_nonpos_nonpos_nonneg (a b : ZFInt) (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a * b

theorem ZFSet.ZFInt.mul_le_mul_left {n m : ZFInt} (k : ZFInt) (h : n ≤ m) (h' : 0 ≤ k) : k * n ≤ k * m

theorem ZFSet.ZFInt.mul_lt_mul_of_pos_left {n m k : ZFInt} (h : n < m) (hk : k > 0) : k * n < k * m

theorem ZFSet.ZFInt.pos_of_mul_pos {a b : ZFInt} (h : 0 < a * b) (ha : 0 < a) : 0 < b

theorem ZFSet.ZFInt.mul_lt_mul_of_pos_right {n m k : ZFInt} (h : n < m) (hk : k > 0) : n * k < m * k

theorem ZFSet.ZFInt.mul_pos_iff {a b : ZFInt} : 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

theorem ZFSet.ZFInt.eq_le_iff {a b : ZFInt} : a = b ↔ a ≤ b ∧ b ≤ a

theorem ZFSet.ZFInt.mul_eq_zero_iff {a b : ZFInt} : a * b = 0 ↔ a = 0 ∨ b = 0

theorem ZFSet.ZFInt.mul_eq_zero_of_ne_zero {a b : ZFInt} : a * b = 0 → a ≠ 0 → b = 0

theorem ZFSet.ZFInt.mul_left_cancel_iff {a b n : ZFInt} (h : n ≠ 0) : n * a = n * b ↔ a = b

theorem ZFSet.ZFInt.mul_right_cancel_iff {a b n : ZFInt} (h : n ≠ 0) : a * n = b * n ↔ a = b

@[implicit_reducible]

noncomputable instance ZFSet.ZFInt.instCommRing_1 : CommRing ZFInt

Equations

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

instance ZFSet.ZFInt.instIsOrderedRing : IsOrderedRing ZFInt

instance ZFSet.ZFInt.instPosMulStrictMono : PosMulStrictMono ZFInt

instance ZFSet.ZFInt.instMulPosStrictMono : MulPosStrictMono ZFInt

@[reducible, inline]

noncomputable abbrev ZFSet.Int : ZFSet.{u_1}

Equations

• ZFSet.Int = ZFSet.Nat.prod {∅} ∪ {∅}.prod ZFSet.Nat

def ZFSet.ZFInt.ofZFNat (n : ZFNat) : ZFInt

Equations

• ZFSet.ZFInt.ofZFNat n = ZFSet.ZFInt.mk (n, 0)

noncomputable def ZFSet.ofInt : ℤ → ZFSet.{u_1}

Equations

• ZFSet.ofInt (Int.ofNat n_1) = ∅.pair ↑↑n_1
• ZFSet.ofInt (Int.negSucc n_1) = (↑(↑n_1 + 1)).pair ∅

noncomputable def ZFSet.toZFInt : ℤ → ZFInt

Equations

• ZFSet.toZFInt (Int.ofNat n_1) = ZFSet.ZFInt.mk (0, ↑n_1)
• ZFSet.toZFInt (Int.negSucc n_1) = ZFSet.ZFInt.mk (↑n_1 + 1, 0)

def ZFSet.PInt' : PSet.{u_1}

Equations

• ZFSet.PInt' = PSet.mk (ULift.{?u.1, 0} ℤ) fun (n : ULift.{?u.1, 0} ℤ) => ZFSet.ofInt'✝ n.down

def ZFSet.Int' : ZFSet.{u_1}

Equations

• ZFSet.Int' = ZFSet.mk ZFSet.PInt'

theorem ZFSet.ZFNat.mem_lift_lift_Nat (n : ℕ) : ↑↑n ∈ Nat

theorem ZFSet.mem_ofInt_Int (n : ℤ) : ofInt n ∈ Int

theorem ZFSet.sub_ofInt_singleton_Int (n : ℤ) : {ofInt n} ⊆ Int

theorem ZFSet.Int.nonempty : Int ≠ ∅

def ZFSet.π₁ (x : ZFSet.{u_1}) : ZFSet.{u_1}

Equations

• x.π₁ = x.sInter.sUnion

noncomputable def ZFSet.π₂ (x : ZFSet.{u_1}) : ZFSet.{u_1}

Equations

• x.π₂ = if x.sUnion \ x.sInter = ∅ then x.π₁ else (x.sUnion \ x.sInter).sUnion

@[simp]

theorem ZFSet.π₁_pair (x y : ZFSet.{u_1}) : (x.pair y).π₁ = x

@[simp]

theorem ZFSet.pair_inter {x y : ZFSet.{u_1}} : {x} ∩ {x, y} = {x}

@[simp]

theorem ZFSet.pair_union {x y : ZFSet.{u_1}} : {x} ∪ {x, y} = {x, y}

@[simp]

theorem ZFSet.pair_minus {x y : ZFSet.{u_1}} : x ≠ y → {x, y} \ {x} = {y}

@[simp]

theorem ZFSet.π₂_pair (x y : ZFSet.{u_1}) : (x.pair y).π₂ = y

theorem ZFSet.pair_eta {z A B : ZFSet.{u_1}} (h : z ∈ A.prod B) : z = z.π₁.pair z.π₂

theorem ZFSet.mem_Int_proj {x : ZFSet.{u_1}} (h : x ∈ Int) : ∃ n ∈ Nat, x.π₁ = ∅ ∧ x.π₂ = n ∨ x.π₁ = n ∧ x.π₂ = ∅

theorem ZFSet.mem_Int_proj' {x : ZFSet.{u_1}} : x ∈ Int → x.π₁ = ∅ ∧ x.π₂ ∈ Nat ∨ x.π₁ ∈ Nat ∧ x.π₂ = ∅

noncomputable def ZFSet.ZFInt.outof : ↥Int → ZFInt

Canonical projection from a set-theoretic integer (an element of ZFSet.Int) to its ZFInt counterpart. Given an element of Int, which by mem_Int_proj' is of the form pair ∅ n or pair n ∅ for some n ∈ Nat, returns mk (0, n) or mk (n, 0) respectively. The definition is deterministic and does not depend on Schröder–Bernstein.

Equations

• ZFSet.ZFInt.outof ⟨n, hn⟩ = if case : n.π₁ = ∅ ∧ n.π₂ ∈ ZFSet.Nat then ZFSet.ZFInt.mk (0, ⟨n.π₂, ⋯⟩) else ZFSet.ZFInt.mk (⟨n.π₁, ⋯⟩, 0)

theorem ZFSet.ZFInt.outof_inj (x y : ↥Int) : outof x = outof y → x = y

theorem ZFSet.ZFNat.mem_Nat_sub_one {n : ZFNat} : ↑(n - 1) ∈ Nat

theorem ZFSet.ZFNat.mem_Nat_sub {n m : ZFNat} : ↑(n - m) ∈ Nat

theorem ZFSet.mem_Int_empty_not_mem {x : ZFSet.{u_1}} {h : x ∈ Int} : ∅ ∉ x

Well-definedness of ZFInt with respect to ZFSet.Int

noncomputable def ZFSet.ZFInt.into (x : ZFInt) : ↥Int

This function maps ZFInt to Int by taking the first projection of the pair.

Equations

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

theorem ZFSet.ZFInt.into_inj_aux (x y : ZFInt) : x.into = y.into → Quotient.out x ≈ Quotient.out y

theorem ZFSet.ZFInt.into_inj (x y : ZFInt) : x.into = y.into → x = y

theorem ZFSet.ZFInt.into.injective : Function.Injective into

theorem ZFSet.ZFInt.outof.injective : Function.Injective outof

noncomputable def ZFSet.ZFInt.EmbeddingZFIntInt : ZFInt ↪ ↥Int

Equations

• ZFSet.ZFInt.EmbeddingZFIntInt = { toFun := ZFSet.ZFInt.into, inj' := ZFSet.ZFInt.into.injective }

noncomputable def ZFSet.ZFInt.EmbeddingIntZFInt : ↥Int ↪ ZFInt

Equations

• ZFSet.ZFInt.EmbeddingIntZFInt = { toFun := ZFSet.ZFInt.outof, inj' := ZFSet.ZFInt.outof.injective }

theorem ZFSet.ZFInt.outof_into (x : ZFInt) : outof x.into = x

outof is a left inverse of into. This is the key fact making outof/into a canonical pair of inverse bijections between ZFInt and {x // x ∈ Int}, removing the need for an abstract Schröder–Bernstein bijection.

theorem ZFSet.ZFInt.into_outof (y : ↥Int) : (outof y).into = y

into is a right inverse of outof.

@[implicit_reducible]

noncomputable instance ZFSet.instLinearOrderSubtypeMemInt : LinearOrder ↥Int

Canonical linear order on the set-theoretic integers, defined as the pullback of the linear order on ZFInt along the canonical projection outof. With this definition, statements like 0 < 1 on {x // x ∈ Int} reduce to the corresponding statements on ZFInt, so they are decidable — unlike the previous Schröder–Bernstein-based definition, which made specific instances of < unprovable.

Equations

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

@[reducible]

noncomputable def ZFSet.instEquivZFIntInt : ZFInt ≃ ↥Int

The type ZFInt is in canonical bijection with the subtype {x // x ∈ ZFSet.Int}. The equivalence is built directly from ZFInt.into and ZFInt.outof — no Schröder–Bernstein, no Classical.choice over a non-empty set of bijections. In particular, instEquivZFIntInt x is deterministic in x.

Equations

• ZFSet.instEquivZFIntInt = { toFun := ZFSet.ZFInt.into, invFun := ZFSet.ZFInt.outof, left_inv := ZFSet.ZFInt.outof_into, right_inv := ZFSet.ZFInt.into_outof }

@[implicit_reducible]

noncomputable instance ZFSet.instCoeZFIntSubtypeMemInt : Coe ZFInt ↥Int

Equations

• ZFSet.instCoeZFIntSubtypeMemInt = { coe := ZFSet.instEquivZFIntInt.toFun }

@[implicit_reducible]

noncomputable instance ZFSet.instCoeSubtypeMemIntZFInt : Coe (↥Int) ZFInt

Equations

• ZFSet.instCoeSubtypeMemIntZFInt = { coe := ZFSet.instEquivZFIntInt.invFun }

theorem ZFSet.instEquivZFIntInt.mono_iff (x y : ↥Int) : instEquivZFIntInt.invFun x < instEquivZFIntInt.invFun y ↔ x < y

The canonical equivalence preserves order: the strict order on {x // x ∈ Int} is exactly the pullback of the strict order on ZFInt along instEquivZFIntInt.invFun = ZFInt.outof.

Euclidean division

ZFInt is equipped with both common integer-division conventions, transported along the canonical ring equivalence from ZFInt to ℤ.

The higher-priority Euclidean-domain instance makes / and % use Int.ediv and Int.emod; for b ≠ 0, its remainder satisfies 0 ≤ a % b < |b|. Floor division remains available through the explicitly named fdiv and fmod operations and through the lower-priority floorEuclideanDomain instance.

instance ZFSet.ZFInt.instNontrivial : Nontrivial ZFInt

instance ZFSet.ZFInt.instCharZero : CharZero ZFInt

noncomputable def ZFSet.ZFInt.equivInt : ZFInt ≃+* ℤ

The canonical ring equivalence between the quotient construction ZFInt and Lean's ℤ.

Equations

• ZFSet.ZFInt.equivInt = (RingEquiv.ofBijective (Int.castRingHom ZFSet.ZFInt) ZFSet.ZFInt.equivInt._proof_2✝).symm

@[simp]

theorem ZFSet.ZFInt.equivInt_intCast (z : ℤ) : equivInt ↑z = z

@[simp]

theorem ZFSet.ZFInt.intCast_equivInt (z : ZFInt) : ↑(equivInt z) = z

theorem ZFSet.ZFInt.equivInt_le (a b : ZFInt) : equivInt a ≤ equivInt b ↔ a ≤ b

theorem ZFSet.ZFInt.equivInt_lt (a b : ZFInt) : equivInt a < equivInt b ↔ a < b

@[simp]

theorem ZFSet.ZFInt.equivInt_abs (z : ZFInt) : equivInt |z| = |equivInt z|

@[reducible]

noncomputable def ZFSet.ZFInt.floorEuclideanDomain : EuclideanDomain ZFInt

The floor-division Euclidean-domain structure on ZFInt.

Equations

• ZFSet.ZFInt.floorEuclideanDomain = ZFSet.ZFInt.equivInt.euclideanDomain

@[reducible]

noncomputable def ZFSet.ZFInt.edivEuclideanDomain : EuclideanDomain ZFInt

The nonnegative-remainder Euclidean-domain structure on ZFInt.

Equations

• ZFSet.ZFInt.edivEuclideanDomain = ZFSet.ZFInt.equivInt.euclideanDomain

@[implicit_reducible, instance 100]

noncomputable instance ZFSet.ZFInt.instFloorEuclideanDomain : EuclideanDomain ZFInt

The floor convention remains available as a lower-priority instance.

Equations

• ZFSet.ZFInt.instFloorEuclideanDomain = ZFSet.ZFInt.floorEuclideanDomain

@[implicit_reducible, instance 10000]

noncomputable instance ZFSet.ZFInt.instEuclideanDomain : EuclideanDomain ZFInt

The ediv convention is the default convention used by / and %.

Equations

• ZFSet.ZFInt.instEuclideanDomain = ZFSet.ZFInt.edivEuclideanDomain

@[simp]

theorem ZFSet.ZFInt.equivInt_div (a b : ZFInt) : equivInt (a / b) = equivInt a / equivInt b

@[simp]

theorem ZFSet.ZFInt.equivInt_mod (a b : ZFInt) : equivInt (a % b) = equivInt a % equivInt b

theorem ZFSet.ZFInt.div_add_mod (a b : ZFInt) : b * (a / b) + a % b = a

theorem ZFSet.ZFInt.mod_nonneg (a : ZFInt) {b : ZFInt} (hb : b ≠ 0) : 0 ≤ a % b

theorem ZFSet.ZFInt.mod_lt_abs (a : ZFInt) {b : ZFInt} (hb : b ≠ 0) : a % b < |b|

@[simp]

theorem ZFSet.ZFInt.mod_eq_zero {a b : ZFInt} : a % b = 0 ↔ b ∣ a

Explicit Euclidean division

noncomputable def ZFSet.ZFInt.ediv (a b : ZFInt) : ZFInt

Euclidean quotient with a nonnegative remainder. This is also the operation used by /.

Equations

• a.ediv b = ZFSet.ZFInt.equivInt.symm (ZFSet.ZFInt.equivInt a / ZFSet.ZFInt.equivInt b)

noncomputable def ZFSet.ZFInt.emod (a b : ZFInt) : ZFInt

Euclidean remainder in the interval [0, |b|) when b ≠ 0. This is also the operation used by %.

Equations

• a.emod b = ZFSet.ZFInt.equivInt.symm (ZFSet.ZFInt.equivInt a % ZFSet.ZFInt.equivInt b)

@[simp]

theorem ZFSet.ZFInt.equivInt_ediv (a b : ZFInt) : equivInt (a.ediv b) = equivInt a / equivInt b

@[simp]

theorem ZFSet.ZFInt.equivInt_emod (a b : ZFInt) : equivInt (a.emod b) = equivInt a % equivInt b

@[simp]

theorem ZFSet.ZFInt.ediv_eq_div (a b : ZFInt) : a.ediv b = a / b

@[simp]

theorem ZFSet.ZFInt.emod_eq_mod (a b : ZFInt) : a.emod b = a % b

theorem ZFSet.ZFInt.ediv_add_emod (a b : ZFInt) : b * a.ediv b + a.emod b = a

theorem ZFSet.ZFInt.emod_nonneg (a : ZFInt) {b : ZFInt} (hb : b ≠ 0) : 0 ≤ a.emod b

theorem ZFSet.ZFInt.emod_lt_abs (a : ZFInt) {b : ZFInt} (hb : b ≠ 0) : a.emod b < |b|

@[simp]

theorem ZFSet.ZFInt.emod_eq_zero {a b : ZFInt} : a.emod b = 0 ↔ b ∣ a

Explicit floor division

noncomputable def ZFSet.ZFInt.fdiv (a b : ZFInt) : ZFInt

Floor quotient: the quotient of a by b, rounded toward negative infinity.

Equations

• a.fdiv b = ZFSet.ZFInt.equivInt.symm ((ZFSet.ZFInt.equivInt a).fdiv (ZFSet.ZFInt.equivInt b))

noncomputable def ZFSet.ZFInt.fmod (a b : ZFInt) : ZFInt

Floor remainder. For a nonzero divisor, it has the sign of the divisor.

Equations

• a.fmod b = ZFSet.ZFInt.equivInt.symm ((ZFSet.ZFInt.equivInt a).fmod (ZFSet.ZFInt.equivInt b))

@[simp]

theorem ZFSet.ZFInt.equivInt_fdiv (a b : ZFInt) : equivInt (a.fdiv b) = (equivInt a).fdiv (equivInt b)

@[simp]

theorem ZFSet.ZFInt.equivInt_fmod (a b : ZFInt) : equivInt (a.fmod b) = (equivInt a).fmod (equivInt b)

theorem ZFSet.ZFInt.fdiv_add_fmod (a b : ZFInt) : b * a.fdiv b + a.fmod b = a

theorem ZFSet.ZFInt.fmod_nonneg_of_pos (a : ZFInt) {b : ZFInt} (hb : 0 < b) : 0 ≤ a.fmod b

theorem ZFSet.ZFInt.fmod_lt_of_pos (a : ZFInt) {b : ZFInt} (hb : 0 < b) : a.fmod b < b

theorem ZFSet.ZFInt.fmod_nonpos_of_neg (a : ZFInt) {b : ZFInt} (hb : b < 0) : a.fmod b ≤ 0

theorem ZFSet.ZFInt.lt_fmod_of_neg (a : ZFInt) {b : ZFInt} (hb : b < 0) : b < a.fmod b

@[simp]

theorem ZFSet.ZFInt.fmod_eq_zero {a b : ZFInt} : a.fmod b = 0 ↔ b ∣ a

Transfer to ℤ

equivInt is registered as a TransferEquiv, so that the transfer tactic reads a goal about ZFInt in ℤ:

example (a b : ZFInt) : a + b = b + a := by
  transfer ZFInt → ℤ =>
    rw [Int.add_comm]

The ring operations, the numerals and the casts travel through the generic map_… lemmas of the transfer_simps simp set; the order relations and the two division conventions are the lemmas proved above, tagged here.

@[implicit_reducible]

noncomputable instance ZFSet.ZFInt.instTransferEquivInt : TransferEquiv ZFInt ℤ

Equivalence used by the transfer tactic to move goals between ZFInt and ℤ.

Equations

• ZFSet.ZFInt.instTransferEquivInt = { equiv := ZFSet.ZFInt.equivInt.toEquiv }

theorem ZFSet.ZFInt.equivInt_dvd (a b : ZFInt) : a ∣ b ↔ equivInt a ∣ equivInt b

Divisibility is read in ℤ; map_dvd_iff reads the wrong way round for transfer.