`mk`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.IntegersFromLogic
domain: Foundation
line: 82 · 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 82.

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

  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`. -/
 108def one : LogicInt := mk (LogicNat.succ LogicNat.zero) LogicNat.zero
 109
 110instance : Zero LogicInt := ⟨zero⟩
 111instance : One LogicInt := ⟨one⟩
 112

papers checked against this theorem

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