`LogicInt`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.IntegersFromLogic on GitHub at line 77.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  74
  75/-- `LogicInt` is the Grothendieck completion of `LogicNat` under
  76addition. -/
  77def LogicInt : Type := Quotient (setoid : Setoid (LogicNat × LogicNat))
  78
  79namespace LogicInt
  80
  81/-- Constructor: form an integer from a pair of naturals. -/
  82def mk (a b : LogicNat) : LogicInt := Quotient.mk' (a, b)
  83
  84/-- Notation `[a, b]ₗ` for the integer `a − b`. Avoids clash with
  85list and matrix notations. -/
  86notation:max "[" a ", " b "]ₗ" => mk a b
  87
  88theorem sound (a b c d : LogicNat) (h : a + d = c + b) :
  89    mk a b = mk c d := by
  90  apply Quotient.sound
  91  show a + d = c + b
  92  exact h
  93
  94/-! ## 3. Embedding LogicNat into LogicInt -/
  95
  96/-- The natural injection `LogicNat ↪ LogicInt` sending `n` to `[n, 0]`.
  97This is the inclusion of the additive monoid into its Grothendieck group. -/
  98def ofLogicNat (n : LogicNat) : LogicInt := mk n LogicNat.zero
  99
 100@[simp] theorem ofLogicNat_zero : ofLogicNat LogicNat.zero = mk LogicNat.zero LogicNat.zero := rfl
 101
 102/-! ## 4. Zero, One, Negation, Addition, Multiplication -/
 103
 104/-- Zero in `LogicInt`. -/
 105def zero : LogicInt := mk LogicNat.zero LogicNat.zero
 106
 107/-- One in `LogicInt`. -/

papers checked against this theorem

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