`one`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.IntegersFromLogic
domain: Foundation
line: 108 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.IntegersFromLogic on GitHub at line 108.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 105def zero : LogicInt := mk LogicNat.zero LogicNat.zero
 106
 107/-- One in `LogicInt`. -/
 108def one : LogicInt := mk (LogicNat.succ LogicNat.zero) LogicNat.zero
 109
 110instance : Zero LogicInt := ⟨zero⟩
 111instance : One LogicInt := ⟨one⟩
 112
 113/-- Negation: `-(a, b) = (b, a)`. -/
 114def neg : LogicInt → LogicInt :=
 115  Quotient.lift (fun (p : LogicNat × LogicNat) => mk p.2 p.1) (by
 116    rintro ⟨a, b⟩ ⟨c, d⟩ h
 117    show mk b a = mk d c
 118    apply sound
 119    show b + c = d + a
 120    rw [eq_iff_toNat_eq, toNat_add, toNat_add]
 121    have h' : toNat a + toNat d = toNat c + toNat b := by
 122      have := congrArg toNat (show a + d = c + b from h)
 123      rwa [toNat_add, toNat_add] at this
 124    omega)
 125
 126instance : Neg LogicInt := ⟨neg⟩
 127
 128/-- Addition: `(a, b) + (c, d) = (a + c, b + d)`. -/
 129def add : LogicInt → LogicInt → LogicInt :=
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.