def
definition
ofLogicInt
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.RationalsFromLogic on GitHub at line 99.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
96/-! ## 3. Embedding LogicInt into LogicRat -/
97
98/-- The natural injection `LogicInt ↪ LogicRat` sending `n` to `n/1`. -/
99def ofLogicInt (n : LogicInt) : LogicRat :=
100 mk n 1 (by
101 intro h
102 have : toInt (1 : LogicInt) = toInt (0 : LogicInt) := congrArg toInt h
103 rw [toInt_one, toInt_zero] at this
104 exact one_ne_zero this)
105
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