zero

formal source

 106/-! ## 4. Zero, One, Negation, Addition, Multiplication -/
 107
 108/-- Zero in `LogicRat`. -/
 109def zero : LogicRat :=
 110  mk 0 1 (by
 111    intro h
 112    have : toInt (1 : LogicInt) = toInt (0 : LogicInt) := congrArg toInt h
 113    rw [toInt_one, toInt_zero] at this
 114    exact one_ne_zero this)
 115
 116/-- One in `LogicRat`. -/
 117def one : LogicRat :=
 118  mk 1 1 (by
 119    intro h
 120    have : toInt (1 : LogicInt) = toInt (0 : LogicInt) := congrArg toInt h
 121    rw [toInt_one, toInt_zero] at this
 122    exact one_ne_zero this)
 123
 124instance : Zero LogicRat := ⟨zero⟩
 125instance : One LogicRat := ⟨one⟩
 126
 127/-- Negation: `-(a/b) = (-a)/b`. -/
 128def neg : LogicRat → LogicRat :=
 129  Quotient.lift
 130    (fun (p : PreRat) => mk (-p.num) p.den p.den_nonzero)
 131    (by
 132      rintro ⟨a, b, hb⟩ ⟨c, d, hd⟩ h
 133      show mk (-a) b hb = mk (-c) d hd
 134      apply sound
 135      show -a * d = -c * b
 136      have h' : a * d = c * b := h
 137      rw [eq_iff_toInt_eq, toInt_mul, toInt_mul, toInt_neg, toInt_neg]
 138      have h'' : toInt a * toInt d = toInt c * toInt b := by
 139        have := congrArg toInt h'