def
definition
def or abbrev
add
show as:
view Lean formalization →
formal statement (Lean)
129def add : LogicInt → LogicInt → LogicInt :=
proof body
Definition body.
130 Quotient.lift₂
131 (fun (p q : LogicNat × LogicNat) => mk (p.1 + q.1) (p.2 + q.2))
132 (by
133 rintro ⟨a, b⟩ ⟨c, d⟩ ⟨a', b'⟩ ⟨c', d'⟩ hab hcd
134 show mk (a + c) (b + d) = mk (a' + c') (b' + d')
135 apply sound
136 show (a + c) + (b' + d') = (a' + c') + (b + d)
137 rw [eq_iff_toNat_eq, toNat_add, toNat_add, toNat_add, toNat_add, toNat_add, toNat_add]
138 have hab_nat : toNat a + toNat b' = toNat a' + toNat b := by
139 have := congrArg toNat (show a + b' = a' + b from hab)
140 rwa [toNat_add, toNat_add] at this
141 have hcd_nat : toNat c + toNat d' = toNat c' + toNat d := by
142 have := congrArg toNat (show c + d' = c' + d from hcd)
143 rwa [toNat_add, toNat_add] at this
144 omega)
145
146instance : Add LogicInt := ⟨add⟩
147
148/-- Multiplication: `(a, b) * (c, d) = (ac + bd, ad + bc)`. -/