ZFC Rational Numbers

This file defines the rational numbers in ZFC, based on the integers and using the ZFInt type.

@[reducible, inline]

abbrev ZFSet.ZFInt' : Type (u_1 + 1)

Equations

• ZFSet.ZFInt' = { x : ZFSet.ZFInt // x ≠ 0 }

@[reducible, inline]

abbrev ZFSet.qrel (p q : ZFInt × ZFInt') : Prop

The equivalence relation on ℤ × ℤ⋆ that defines the rational numbers.

Equations

• ZFSet.qrel p q = (p.1 * ↑q.2 = ↑p.2 * q.1)

def ZFSet.qrel_eq : Equivalence ZFSet.qrel

Equations

• ZFSet.qrel_eq = ⋯

@[implicit_reducible]

instance ZFSet.instSetoidZFIntZFInt' : Setoid (ZFInt × ZFInt')

ℤ × ℤ⋆ equipped with qrel is a setoid.

Equations

• ZFSet.instSetoidZFIntZFInt' = { r := ZFSet.qrel, iseqv := ZFSet.qrel_eq }

@[reducible, inline]

abbrev ZFSet.ZFRat : Type (u_1 + 1)

ℚ is defined as ℤ × ℤ⋆ quotiented by qrel

Equations

• ZFSet.ZFRat = Quotient ZFSet.instSetoidZFIntZFInt'

def ZFSet.ZFRat.mk : ZFInt × ZFInt' → ZFRat

Equations

• ZFSet.ZFRat.mk = Quotient.mk''

@[simp]

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

@[simp]

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

theorem ZFSet.ZFRat.eq {x y : ZFInt × ZFInt'} : mk x = mk y ↔ ZFSet.qrel x y

theorem ZFSet.ZFRat.sound {x y : ZFInt × ZFInt'} (h : ZFSet.qrel x y) : mk x = mk y

theorem ZFSet.ZFRat.exact {x y : ZFInt × ZFInt'} : mk x = mk y → ZFSet.qrel x y

@[reducible, inline]

abbrev ZFSet.ZFRat.zero : ZFRat

Equations

• ZFSet.ZFRat.zero = ZFSet.ZFRat.mk (0, ⟨1, ZFSet.ZFInt.one_ne_zero⟩)

@[reducible, inline]

abbrev ZFSet.ZFRat.one : ZFRat

Equations

• ZFSet.ZFRat.one = ZFSet.ZFRat.mk (1, ⟨1, ZFSet.ZFInt.one_ne_zero⟩)

@[implicit_reducible]

instance ZFSet.ZFRat.instZero : Zero ZFRat

Equations

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

@[implicit_reducible]

instance ZFSet.ZFRat.instOne : One ZFRat

Equations

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

@[implicit_reducible]

instance ZFSet.ZFRat.instInhabited : Inhabited ZFRat

Equations

• ZFSet.ZFRat.instInhabited = { default := 0 }

theorem ZFSet.ZFRat.zero_eq : 0 = mk (0, ⟨1, ZFInt.one_ne_zero⟩)

theorem ZFSet.ZFRat.one_eq : 1 = mk (1, ⟨1, ZFInt.one_ne_zero⟩)

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

theorem ZFSet.ZFRat.mk_ne_zero {a : ZFInt} {b : ZFInt'} (ha : a ≠ 0) : mk (a, b) ≠ 0

theorem ZFSet.ZFRat.mk_eq_one_iff {n : ZFInt} {m : ZFInt'} : mk (n, m) = 1 ↔ n = ↑m

theorem ZFSet.ZFRat.one_ne_zero : 1 ≠ 0

@[reducible, inline]

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

Equations

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

@[implicit_reducible]

noncomputable instance ZFSet.ZFRat.instAdd : Add ZFRat

Equations

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

theorem ZFSet.ZFRat.add_eq (n m : ZFInt × ZFInt') : mk n + mk m = mk (n.1 * ↑m.2 + ↑n.2 * m.1, ⟨↑n.2 * ↑m.2, ⋯⟩)

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

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

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

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

@[simp]

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

@[simp]

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

@[reducible, inline]

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

Equations

• n.neg = Quotient.liftOn n (fun (x : ZFSet.ZFInt × ZFSet.ZFInt') => match x with | (x, y) => ZFSet.ZFRat.mk (-x, y)) ZFSet.ZFRat.neg._proof_2

@[implicit_reducible]

instance ZFSet.ZFRat.instNeg : Neg ZFRat

Equations

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

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

@[simp]

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

@[simp]

theorem ZFSet.ZFRat.neg_zero : -0 = 0

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[reducible, inline]

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

Equations

• n.sub m = n + -m

@[implicit_reducible]

noncomputable instance ZFSet.ZFRat.instSub : Sub ZFRat

Equations

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

theorem ZFSet.ZFRat.sub_eq (n m : ZFInt × ZFInt') : mk n - mk m = mk (n.1 * ↑m.2 - m.1 * ↑n.2, ⟨↑n.2 * ↑m.2, ⋯⟩)

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[implicit_reducible]

noncomputable instance ZFSet.ZFRat.instMul : Mul ZFRat

Equations

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

theorem ZFSet.ZFRat.mul_eq (n m : ZFInt × ZFInt') : mk n * mk m = mk (n.1 * m.1, ⟨↑n.2 * ↑m.2, ⋯⟩)

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

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

@[implicit_reducible]

noncomputable instance ZFSet.ZFRat.instCommRing : CommRing ZFRat

Equations

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

theorem ZFSet.ZFRat.intCast_eq_mk (n : ℤ) : ↑n = mk (↑n, ⟨1, ZFInt.one_ne_zero⟩)

@[reducible, inline]

abbrev ZFSet.ZFRat.ZFRat' : Type (u_1 + 1)

Equations

• ZFSet.ZFRat.ZFRat' = { x : ZFSet.ZFRat // x ≠ 0 }

@[reducible, inline]

noncomputable abbrev ZFSet.ZFRat.inv : ZFRat' → ZFRat'

Equations

• ZFSet.ZFRat.inv ⟨x_1, hx⟩ = ⟨ZFSet.ZFRat.mk (↑(Quotient.out x_1).2, ⟨(Quotient.out x_1).1, ⋯⟩), ⋯⟩

@[implicit_reducible]

noncomputable instance ZFSet.ZFRat.instInvZFRat' : Inv ZFRat'

Equations

• ZFSet.ZFRat.instInvZFRat' = { inv := ZFSet.ZFRat.inv }

@[implicit_reducible]

noncomputable instance ZFSet.ZFRat.instInv : Inv ZFRat

Equations

• ZFSet.ZFRat.instInv = { inv := fun (x : ZFSet.ZFRat) => if hx : x ≠ 0 then ↑(ZFSet.ZFRat.inv ⟨x, hx⟩) else 0 }

theorem ZFSet.ZFRat.inv_eq {a : ZFRat} (ha : a ≠ 0) : a⁻¹ = ↑⟨a, ha⟩⁻¹

@[reducible, inline]

noncomputable abbrev ZFSet.ZFRat.hdiv (n : ZFRat) (m : ZFRat') : ZFRat

Equations

• n.hdiv m = n * ↑m⁻¹

@[reducible, inline]

noncomputable abbrev ZFSet.ZFRat.div (n m : ZFRat) : ZFRat

Equations

• n.div m = if hm : m ≠ 0 then n.hdiv ⟨m, hm⟩ else 0

@[implicit_reducible]

noncomputable instance ZFSet.ZFRat.instHDivZFRat' : HDiv ZFRat ZFRat' ZFRat

Equations

• ZFSet.ZFRat.instHDivZFRat' = { hDiv := ZFSet.ZFRat.hdiv }

@[implicit_reducible]

noncomputable instance ZFSet.ZFRat.instDiv : Div ZFRat

Equations

• ZFSet.ZFRat.instDiv = { div := ZFSet.ZFRat.div }

theorem ZFSet.ZFRat.div_eq {n m : ZFRat} (hm : m ≠ 0) : n / m = n / ↑⟨m, hm⟩

theorem ZFSet.ZFRat.div_eq_mul_inv {n m : ZFRat} (hm : m ≠ 0) : n / m = n * ↑⟨m, hm⟩⁻¹

@[simp]

theorem ZFSet.ZFRat.mul_inv' {a : ZFRat'} : ↑a * ↑a⁻¹ = 1

@[simp]

theorem ZFSet.ZFRat.mul_inv {a : ZFRat} (ha : a ≠ 0) : a * a⁻¹ = 1

@[simp]

theorem ZFSet.ZFRat.inv_mul' {a : ZFRat'} : ↑a⁻¹ * ↑a = 1

@[simp]

theorem ZFSet.ZFRat.inv_mul {a : ZFRat} (ha : a ≠ 0) : a⁻¹ * a = 1

theorem ZFSet.ZFRat.mk_eq_div (a : ZFInt) (b : ZFInt') : mk (a, b) = mk (a, ⟨1, ZFInt.one_ne_zero⟩) / mk (↑b, ⟨1, ZFInt.one_ne_zero⟩)

@[implicit_reducible]

noncomputable instance ZFSet.ZFRat.instRatCast : RatCast ZFRat

Equations

• ZFSet.ZFRat.instRatCast = { ratCast := fun (q : ℚ) => ↑q.num / ↑q.den }

noncomputable def ZFSet.ZFRat.qsmul (k : ℚ) (m : ZFRat) : ZFRat

Equations

• ZFSet.ZFRat.qsmul k m = ↑k * m

noncomputable def ZFSet.ZFRat.nnqsmul : ℚ≥0 → ZFRat → ZFRat

Equations

• ZFSet.ZFRat.nnqsmul ⟨k, property⟩ m = ZFSet.ZFRat.qsmul k m

@[implicit_reducible]

noncomputable instance ZFSet.ZFRat.instDivisionRing : DivisionRing ZFRat

Equations

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

@[implicit_reducible]

noncomputable instance ZFSet.ZFRat.instField : Field ZFRat

Equations

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

def ZFSet.ZFRat.isPos (x : ZFRat) : Prop

A rational is positive iff numerator and denominator carry the same sign. Well-defined because for equivalent reps (a,b) ≈ (c,d) (i.e. a*d = b*c), multiplying both sides by b*d gives (a*b)*(d*d) = (b*b)*(c*d), and b*b, d*d are both positive, so a*b and c*d share a sign.

Equations

• x.isPos = Quotient.liftOn x (fun (x : ZFSet.ZFInt × ZFSet.ZFInt') => match x with | (a, ⟨b, property⟩) => 0 < a * b) ZFSet.ZFRat.isPos._proof_1✝

def ZFSet.ZFRat.lt (x y : ZFRat) : Prop

Equations

• x.lt y = (y - x).isPos

@[implicit_reducible]

instance ZFSet.ZFRat.instLT : LT ZFRat

Equations

• ZFSet.ZFRat.instLT = { lt := ZFSet.ZFRat.lt }

@[implicit_reducible]

instance ZFSet.ZFRat.instLE : LE ZFRat

Equations

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

theorem ZFSet.ZFRat.isPos_eq (n : ZFInt × ZFInt') : (mk n).isPos ↔ 0 < n.1 * ↑n.2

theorem ZFSet.ZFRat.lt_eq (n m : ZFInt × ZFInt') : mk n < mk m ↔ 0 < (m.1 * ↑n.2 - n.1 * ↑m.2) * (↑m.2 * ↑n.2)

theorem ZFSet.ZFRat.isPos_trichotomy (x : ZFRat) : x.isPos ∨ x = 0 ∨ (-x).isPos

theorem ZFSet.ZFRat.not_isPos_zero : ¬isPos 0

theorem ZFSet.ZFRat.isPos_one : isPos 1

theorem ZFSet.ZFRat.isPos_add {x y : ZFRat} (hx : x.isPos) (hy : y.isPos) : (x + y).isPos

theorem ZFSet.ZFRat.isPos_mul {x y : ZFRat} (hx : x.isPos) (hy : y.isPos) : (x * y).isPos

theorem ZFSet.ZFRat.lt_irrefl (x : ZFRat) : ¬x < x

theorem ZFSet.ZFRat.not_isPos_and_isPos_neg {z : ZFRat} (h : z.isPos) : ¬(-z).isPos

theorem ZFSet.ZFRat.lt_asymm {x y : ZFRat} (h : x < y) : ¬y < x

theorem ZFSet.ZFRat.lt_trans {x y z : ZFRat} (hxy : x < y) (hyz : y < z) : x < z

theorem ZFSet.ZFRat.lt_trichotomy (x y : ZFRat) : x < y ∨ x = y ∨ y < x

theorem ZFSet.ZFRat.le_refl (x : ZFRat) : x ≤ x

theorem ZFSet.ZFRat.le_trans {x y z : ZFRat} (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z

theorem ZFSet.ZFRat.le_antisymm {x y : ZFRat} (hxy : x ≤ y) (hyx : y ≤ x) : x = y

theorem ZFSet.ZFRat.le_total (x y : ZFRat) : x ≤ y ∨ y ≤ x

theorem ZFSet.ZFRat.lt_iff_le_not_ge (x y : ZFRat) : x < y ↔ x ≤ y ∧ ¬y ≤ x

@[implicit_reducible]

noncomputable instance ZFSet.ZFRat.instLinearOrder : LinearOrder ZFRat

Equations

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

theorem ZFSet.ZFRat.add_le_add_left (a b : ZFRat) (h : a ≤ b) (c : ZFRat) : a + c ≤ b + c

theorem ZFSet.ZFRat.zero_lt_one : 0 < 1

theorem ZFSet.ZFRat.zero_le_one : 0 ≤ 1

theorem ZFSet.ZFRat.mul_lt_mul_of_pos_left {a : ZFRat} (ha : 0 < a) {b c : ZFRat} (hbc : b < c) : a * b < a * c

theorem ZFSet.ZFRat.mul_lt_mul_of_pos_right {a : ZFRat} (ha : 0 < a) {b c : ZFRat} (hbc : b < c) : b * a < c * a

theorem ZFSet.ZFRat.mul_le_mul_of_nonneg_left {a : ZFRat} (ha : 0 ≤ a) {b c : ZFRat} (hbc : b ≤ c) : a * b ≤ a * c

theorem ZFSet.ZFRat.mul_le_mul_of_nonneg_right {a : ZFRat} (ha : 0 ≤ a) {b c : ZFRat} (hbc : b ≤ c) : b * a ≤ c * a

instance ZFSet.ZFRat.instIsOrderedRing : IsOrderedRing ZFRat

instance ZFSet.ZFRat.instPosMulStrictMono : PosMulStrictMono ZFRat

instance ZFSet.ZFRat.instMulPosStrictMono : MulPosStrictMono ZFRat

Transfer to ℚ

ZFRat and ℚ are the same field: the ring morphism ℚ →+* ZFRat given by the RatCast instance is injective because ZFRat has characteristic zero, and surjective because every mk (a, b) is the quotient of the images of two integers. The resulting equivalence is registered as a TransferEquiv, so that the transfer tactic reads a goal about ZFRat in ℚ:

example (x y : ZFRat) : x + y = y + x := by
  transfer ZFRat → ℚ =>
    rw [add_comm]

The field operations, the numerals and the casts travel through the generic map_… lemmas of the transfer_simps simp set; the order relations are tagged below.

instance ZFSet.ZFRat.instCharZero : CharZero ZFRat

noncomputable def ZFSet.ZFRat.equivRat : ZFRat ≃+* ℚ

The canonical ring equivalence between the quotient construction ZFRat and Lean's ℚ.

Equations

• ZFSet.ZFRat.equivRat = (RingEquiv.ofBijective (Rat.castHom ZFSet.ZFRat) ZFSet.ZFRat.equivRat._proof_2✝).symm

@[simp]

theorem ZFSet.ZFRat.equivRat_ratCast (q : ℚ) : equivRat ↑q = q

@[simp]

theorem ZFSet.ZFRat.ratCast_equivRat (x : ZFRat) : ↑(equivRat x) = x

theorem ZFSet.ZFRat.equivRat_le (a b : ZFRat) : equivRat a ≤ equivRat b ↔ a ≤ b

theorem ZFSet.ZFRat.equivRat_lt (a b : ZFRat) : equivRat a < equivRat b ↔ a < b

@[implicit_reducible]

noncomputable instance ZFSet.ZFRat.instTransferEquivRat : TransferEquiv ZFRat ℚ

Equivalence used by the transfer tactic to move goals between ZFRat and ℚ.

Equations

• ZFSet.ZFRat.instTransferEquivRat = { equiv := ZFSet.ZFRat.equivRat.toEquiv }