structure Section_4_2.PreRat : Type

• numerator : ℤ
• denominator : ℤ
• nonzero : self.denominator ≠ 0

@[implicit_reducible]

instance Section_4_2.PreRat.instSetoid : Setoid PreRat

Exercise 4.2.1

Equations

• Section_4_2.PreRat.instSetoid = { r := fun (a b : Section_4_2.PreRat) => a.numerator * b.denominator = b.numerator * a.denominator, iseqv := ⋯ }

@[simp]

theorem Section_4_2.PreRat.eq (a b c d : ℤ) (hb : b ≠ 0) (hd : d ≠ 0) : { numerator := a, denominator := b, nonzero := hb } ≈ { numerator := c, denominator := d, nonzero := hd } ↔ a * d = c * b

@[reducible, inline]

abbrev Section_4_2.Rat : Type

Equations

• Section_4_2.Rat = Quotient Section_4_2.PreRat.instSetoid

@[reducible, inline]

abbrev Section_4_2.Rat.formalDiv (a b : ℤ) : Rat

We give division a "junk" value of 0//1 if the denominator is zero

Equations

• a // b = ⟦if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h } else { numerator := 0, denominator := 1, nonzero := Section_4_2.Rat.formalDiv._proof_1 }⟧

def Section_4_2.«term_//_» : Lean.TrailingParserDescr

Equations

• Section_4_2.«term_//_» = Lean.ParserDescr.trailingNode `Section_4_2.«term_//_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " // ") (Lean.ParserDescr.cat `term 101))

theorem Section_4_2.Rat.eq (a c : ℤ) {b d : ℤ} (hb : b ≠ 0) (hd : d ≠ 0) : a // b = c // d ↔ a * d = c * b

Definition 4.2.1 (Rationals)

theorem Section_4_2.Rat.eq_diff (n : Rat) : ∃ (a : ℤ) (b : ℤ), b ≠ 0 ∧ n = a // b

Definition 4.2.1 (Rationals)

@[implicit_reducible]

instance Section_4_2.Rat.decidableEq : DecidableEq Rat

Decidability of equality. Hint: modify the proof of DecidableEq Int from the previous section. However, because formal division handles the case of zero denominator separately, it may be more convenient to avoid that operation and work directly with the Quotient API.

Equations

• Section_4_2.Rat.decidableEq = sorry

@[implicit_reducible]

instance Section_4_2.Rat.add_inst : Add Rat

Lemma 4.2.3 (Addition well-defined)

Equations

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

theorem Section_4_2.Rat.add_eq (a c : ℤ) {b d : ℤ} (hb : b ≠ 0) (hd : d ≠ 0) : a // b + c // d = (a * d + b * c) // (b * d)

Definition 4.2.2 (Addition of rationals)

@[implicit_reducible]

instance Section_4_2.Rat.mul_inst : Mul Rat

Lemma 4.2.3 (Multiplication well-defined)

Equations

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

theorem Section_4_2.Rat.mul_eq (a c : ℤ) {b d : ℤ} (hb : b ≠ 0) (hd : d ≠ 0) : a // b * c // d = (a * c) // (b * d)

Definition 4.2.2 (Multiplication of rationals)

@[implicit_reducible]

instance Section_4_2.Rat.neg_inst : Neg Rat

Lemma 4.2.3 (Negation well-defined)

Equations

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

theorem Section_4_2.Rat.neg_eq (a : ℤ) {b : ℤ} (hb : b ≠ 0) : -a // b = (-a) // b

Definition 4.2.2 (Negation of rationals)

@[implicit_reducible]

instance Section_4_2.Rat.instIntCast : IntCast Rat

Embedding the integers in the rationals

Equations

• Section_4_2.Rat.instIntCast = { intCast := fun (a : ℤ) => a // 1 }

@[implicit_reducible]

instance Section_4_2.Rat.instNatCast : NatCast Rat

Equations

• Section_4_2.Rat.instNatCast = { natCast := fun (n : ℕ) => ↑n // 1 }

@[implicit_reducible]

instance Section_4_2.Rat.instOfNat {n : ℕ} : OfNat Rat n

Equations

• Section_4_2.Rat.instOfNat = { ofNat := ↑n // 1 }

theorem Section_4_2.Rat.coe_Int_eq (a : ℤ) : ↑a = a // 1

theorem Section_4_2.Rat.coe_Nat_eq (n : ℕ) : ↑n = ↑n // 1

theorem Section_4_2.Rat.of_Nat_eq (n : ℕ) : OfNat.ofNat n = ↑(OfNat.ofNat n) // 1

theorem Section_4_2.Rat.natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1

natCast distributes over successor

theorem Section_4_2.Rat.intCast_add (a b : ℤ) : ↑a + ↑b = ↑(a + b)

intCast distributes over addition

theorem Section_4_2.Rat.intCast_mul (a b : ℤ) : ↑a * ↑b = ↑(a * b)

intCast distributes over multiplication

theorem Section_4_2.Rat.intCast_neg (a : ℤ) : -↑a = ↑(-a)

intCast commutes with negation

theorem Section_4_2.Rat.coe_Int_inj : Function.Injective fun (n : ℤ) => ↑n

@[implicit_reducible]

instance Section_4_2.Rat.instInv : Inv Rat

Whereas the book leaves the inverse of 0 undefined, it is more convenient in Lean to assign a "junk" value to this inverse; we arbitrarily choose this junk value to be 0.

Equations

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

theorem Section_4_2.Rat.inv_eq (a : ℤ) {b : ℤ} (hb : b ≠ 0) : (a // b)⁻¹ = b // a

@[simp]

theorem Section_4_2.Rat.inv_zero : 0⁻¹ = 0

@[implicit_reducible]

instance Section_4_2.Rat.addGroup_inst : AddGroup Rat

Proposition 4.2.4 (laws of algebra) / Exercise 4.2.3

Equations

• Section_4_2.Rat.addGroup_inst = AddGroup.ofLeftAxioms Section_4_2.Rat.addGroup_inst._proof_1 ⋯ ⋯

@[implicit_reducible]

instance Section_4_2.Rat.instAddCommGroup : AddCommGroup Rat

Proposition 4.2.4 (laws of algebra) / Exercise 4.2.3

Equations

• Section_4_2.Rat.instAddCommGroup = { toAddGroup := Section_4_2.Rat.addGroup_inst, add_comm := ⋯ }

@[implicit_reducible]

instance Section_4_2.Rat.instCommMonoid : CommMonoid Rat

Proposition 4.2.4 (laws of algebra) / Exercise 4.2.3

Equations

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

@[implicit_reducible]

instance Section_4_2.Rat.instCommRing : CommRing Rat

Proposition 4.2.4 (laws of algebra) / Exercise 4.2.3

Equations

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

@[implicit_reducible]

instance Section_4_2.Rat.instRatCast : RatCast Rat

Equations

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

theorem Section_4_2.Rat.ratCast_inj : Function.Injective fun (n : ℚ) => ↑n

theorem Section_4_2.Rat.coe_Rat_eq (a : ℤ) {b : ℤ} (hb : b ≠ 0) : ↑(↑a / ↑b) = a // b

@[implicit_reducible]

instance Section_4_2.Rat.instDivInvMonoid : DivInvMonoid Rat

Default definition of division

Equations

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

theorem Section_4_2.Rat.div_eq (q r : Rat) : q / r = q * r⁻¹

@[implicit_reducible]

instance Section_4_2.Rat.instField : Field Rat

Proposition 4.2.4 (laws of algebra) / Exercise 4.2.3

Equations

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

theorem Section_4_2.Rat.sub_eq (a b : Rat) : a - b = a + -b

Definition of subtraction

def Section_4_2.Rat.coe_int_hom : ℤ →+* Rat

Equations

• Section_4_2.Rat.coe_int_hom = { toFun := fun (n : ℤ) => ↑n, map_one' := Section_4_2.Rat.coe_int_hom._proof_1, map_mul' := ⋯, map_zero' := Section_4_2.Rat.coe_int_hom._proof_2, map_add' := ⋯ }

def Section_4_2.Rat.isPos (q : Rat) : Prop

Definition 4.2.6 (positivity)

Equations

• q.isPos = ∃ (a : ℤ) (b : ℤ), a > 0 ∧ b > 0 ∧ q = ↑a / ↑b

def Section_4_2.Rat.isNeg (q : Rat) : Prop

Definition 4.2.6 (negativity)

Equations

• q.isNeg = ∃ (r : Section_4_2.Rat), r.isPos ∧ q = -r

theorem Section_4_2.Rat.trichotomous (x : Rat) : x = 0 ∨ x.isPos ∨ x.isNeg

Lemma 4.2.7 (trichotomy of rationals) / Exercise 4.2.4

theorem Section_4_2.Rat.not_zero_and_pos (x : Rat) : ¬(x = 0 ∧ x.isPos)

Lemma 4.2.7 (trichotomy of rationals) / Exercise 4.2.4

theorem Section_4_2.Rat.not_zero_and_neg (x : Rat) : ¬(x = 0 ∧ x.isNeg)

Lemma 4.2.7 (trichotomy of rationals) / Exercise 4.2.4

theorem Section_4_2.Rat.not_pos_and_neg (x : Rat) : ¬(x.isPos ∧ x.isNeg)

Lemma 4.2.7 (trichotomy of rationals) / Exercise 4.2.4

@[implicit_reducible]

instance Section_4_2.Rat.instLT : LT Rat

Definition 4.2.8 (Ordering of the rationals)

Equations

• Section_4_2.Rat.instLT = { lt := fun (x y : Section_4_2.Rat) => (x - y).isNeg }

@[implicit_reducible]

instance Section_4_2.Rat.instLE : LE Rat

Definition 4.2.8 (Ordering of the rationals)

Equations

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

theorem Section_4_2.Rat.lt_iff (x y : Rat) : x < y ↔ (x - y).isNeg

theorem Section_4_2.Rat.le_iff (x y : Rat) : x ≤ y ↔ x < y ∨ x = y

theorem Section_4_2.Rat.gt_iff (x y : Rat) : x > y ↔ (x - y).isPos

theorem Section_4_2.Rat.ge_iff (x y : Rat) : x ≥ y ↔ x > y ∨ x = y

theorem Section_4_2.Rat.trichotomous' (x y : Rat) : x > y ∨ x < y ∨ x = y

Proposition 4.2.9(a) (order trichotomy) / Exercise 4.2.5

theorem Section_4_2.Rat.not_gt_and_lt (x y : Rat) : ¬(x > y ∧ x < y)

Proposition 4.2.9(a) (order trichotomy) / Exercise 4.2.5

theorem Section_4_2.Rat.not_gt_and_eq (x y : Rat) : ¬(x > y ∧ x = y)

Proposition 4.2.9(a) (order trichotomy) / Exercise 4.2.5

theorem Section_4_2.Rat.not_lt_and_eq (x y : Rat) : ¬(x < y ∧ x = y)

Proposition 4.2.9(a) (order trichotomy) / Exercise 4.2.5

theorem Section_4_2.Rat.antisymm (x y : Rat) : x < y ↔ y > x

Proposition 4.2.9(b) (order is anti-symmetric) / Exercise 4.2.5

theorem Section_4_2.Rat.lt_trans {x y z : Rat} (hxy : x < y) (hyz : y < z) : x < z

Proposition 4.2.9(c) (order is transitive) / Exercise 4.2.5

theorem Section_4_2.Rat.add_lt_add_right {x y : Rat} (z : Rat) (hxy : x < y) : x + z < y + z

Proposition 4.2.9(d) (addition preserves order) / Exercise 4.2.5

theorem Section_4_2.Rat.mul_lt_mul_right {x y z : Rat} (hxy : x < y) (hz : z.isPos) : x * z < y * z

Proposition 4.2.9(e) (positive multiplication preserves order) / Exercise 4.2.5

@[implicit_reducible]

instance Section_4_2.Rat.decidableRel : DecidableRel fun (x1 x2 : Rat) => x1 ≤ x2

(Not from textbook) Establish the decidability of this order.

Equations

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

@[implicit_reducible]

instance Section_4_2.Rat.instLinearOrder : LinearOrder Rat

(Not from textbook) Rat has the structure of a linear ordering.

Equations

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

instance Section_4_2.Rat.instIsStrictOrderedRing : IsStrictOrderedRing Rat

(Not from textbook) Rat has the structure of a strict ordered ring.

theorem Section_4_2.Rat.mul_lt_mul_right_of_neg (x y z : Rat) (hxy : x < y) (hz : z.isNeg) : x * z > y * z

Exercise 4.2.6

@[reducible, inline]

abbrev Section_4_2.Rat.equivRat : Rat ≃ ℚ

Not in textbook: create an equivalence between Rat and ℚ. This requires some familiarity with the API for Mathlib's version of the rationals.

Equations

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

@[reducible, inline]

abbrev Section_4_2.Rat.equivRat_order : Rat ≃o ℚ

Not in textbook: equivalence preserves order

Equations

• Section_4_2.Rat.equivRat_order = { toEquiv := Section_4_2.Rat.equivRat, map_rel_iff' := ⋯ }

@[reducible, inline]

abbrev Section_4_2.Rat.equivRat_ring : Rat ≃+* ℚ

Not in textbook: equivalence preserves ring operations

Equations

• Section_4_2.Rat.equivRat_ring = { toEquiv := Section_4_2.Rat.equivRat, map_mul' := ⋯, map_add' := ⋯ }

def Section_4_2.Rat.equivRat_ring_symm : ℚ ≃+* Rat

(Not from textbook) The textbook rationals are isomorphic (as a field) to the Mathlib rationals.

Equations

• Section_4_2.Rat.equivRat_ring_symm = Section_4_2.Rat.equivRat_ring.symm