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)

Imported ZFLean declaration.

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)

theorem ZFSet.qrel_eq : Equivalence ZFSet.qrel

@[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

Imported ZFLean declaration.

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

Imported ZFLean declaration.

Equations

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

@[reducible, inline]

abbrev ZFSet.ZFRat.one : ZFRat

Imported ZFLean declaration.

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_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

Imported ZFLean declaration.

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

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

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

@[reducible, inline]

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

Imported ZFLean declaration.

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_1

@[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)

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

theorem ZFSet.ZFRat.neg_zero : -0 = 0

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

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

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

@[reducible, inline]

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

Rational subtraction in the ZF rational model.

Equations

• n.sub m = n + -m

@[implicit_reducible]

noncomputable instance ZFSet.ZFRat.instSub : Sub ZFRat

Imported ZFLean declaration.

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

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

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

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

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

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

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.mul (n m : ZFRat) : ZFRat

Imported ZFLean declaration.

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

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

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)

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

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.

@[reducible, inline]

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

The subtype of nonzero ZF rational numbers.

Equations

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

@[reducible, inline]

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

Imported ZFLean declaration.

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

Division by a nonzero ZF rational.

Equations

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

@[reducible, inline]

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

Division on ZF rational numbers, with division by zero sent to zero.

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

Imported ZFLean declaration.

Equations

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

@[implicit_reducible]

noncomputable instance ZFSet.ZFRat.instDiv : Div ZFRat

Imported ZFLean declaration.

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

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

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

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

@[implicit_reducible]

noncomputable instance ZFSet.ZFRat.instRatCast : RatCast ZFRat

Equations

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

@[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.