danabra.mov
My solutions to Tao's Analysis I, formalized in Lean
formatting for Ch 2; add some tactic examples
+94
-66
+1
analysis/Analysis/Misc/SIExamples.lean
+1
analysis/Analysis/Misc/SIExamples.lean
···
14
14
#check E = m * c**2
15
15
#check E = m * v**2 / 2 + m * g * h
16
16
-- #check E = m * c**3 -- fails to typecheck
17
+
-- #check m + v -- fails to typecheck
17
18
18
19
example (hv : v = 60 • kilo meter / hour) : (StandardUnit _).in v = 50/(3:ℝ) := by
19
20
simp [←Scalar.val_inj, hour, minute, kilo, meter, second, hv]
+8
-2
analysis/Analysis/Misc/UnitsSystemExamples.lean
+8
-2
analysis/Analysis/Misc/UnitsSystemExamples.lean
···
4
4
open UnitsSystem
5
5
variable [UnitsSystem]
6
6
7
-
-- Many algebraic identities involving `Scalar` can be established by first using `←toFormal_inj`
8
-
-- to coerce to `Formal`, using `simp` to push coercions inside, then appealing to `ring`. We give some examples below.
7
+
/- Many algebraic identities involving `Scalar` can be established by first using `simp [←toFormal_inj]` to coerce to `Formal` and push coercions inside, then appealing to `ring`. We give some examples below.
8
+
9
+
Alternatively, one can "work in coordinates" by using `simp [←val_inj]` in place of `simp [←toFormal_inj]`.
10
+
-/
9
11
10
12
/-- A cast is needed here because `(d₁+d₂)+d₃` is not definitionally equal to `d₁+(d₂+d₃)`. -/
11
13
theorem UnitsSystem.Scalar.hMul_assoc {d₁ d₂ d₃:Dimensions} (a:Scalar d₁) (b:Scalar d₂) (c:Scalar d₃):
···
23
25
/-- A cast is needed here because `2 • d` is not definitionally equal to `d+d`. -/
24
26
theorem UnitsSystem.Scalar.sq_add {d:Dimensions} (a b:Scalar d) : (a+b)**2 = a**2 + (2 • a * b).cast + b**2 := by
25
27
simp [←toFormal_inj]; ring
28
+
29
+
/-- An alternate proof based on working in coordinates-/
30
+
theorem UnitsSystem.Scalar.sq_add' {d:Dimensions} (a b:Scalar d) : (a+b)**2 = a**2 + (2 • a * b).cast + b**2 := by
31
+
simp [←val_inj]; ring
+9
-9
analysis/Analysis/Section_2_1.lean
+9
-9
analysis/Analysis/Section_2_1.lean
···
1
1
import Mathlib.Tactic
2
2
3
3
/-!
4
-
# Analysis I, Section 2.1
4
+
# Analysis I, Section 2.1: The Peano Axioms
5
5
6
6
This file is a translation of Section 2.1 of Analysis I to Lean 4. All numbering refers to the
7
7
original text.
···
18
18
Chapter2 namespace. (In the book, the natural numbers are treated in a purely axiomatic
19
19
fashion, as a type that obeys the Peano axioms; but here we take advantage of Lean's native
20
20
inductive types to explicitly construct a version of the natural numbers that obey those
21
-
axioms. One could also proceed more axiomatically, as is done in Section 3 for set theory, but
22
-
we leave this as an exercise for the reader.)
23
-
- Establishment of the Peano axioms for `Chapter2.Nat`
24
-
- Recursive definitions for `Chapter2.Nat`
21
+
axioms. One could also proceed more axiomatically, as is done in Section 3 for set theory:
22
+
see the epilogue to this chapter.)
23
+
- Establishment of the Peano axioms for `Chapter2.Nat`.
24
+
- Recursive definitions for `Chapter2.Nat`.
25
25
26
-
Note: at the end of this Chapter, the `Chapter2.Nat` class will be deprecated in favor of the
26
+
Note: at the end of this chapter, the `Chapter2.Nat` class will be deprecated in favor of the
27
27
standard Mathlib class `_root_.Nat`, or `ℕ`. However, we will develop the properties of
28
28
`Chapter2.Nat` "by hand" in the next few sections for pedagogical purposes.
29
29
···
52
52
53
53
/--
54
54
Definition 2.1.3 (Definition of the numerals 0, 1, 2, etc.). Note: to avoid ambiguity, one may
55
-
need to use explicit casts such as (0:Nat), (1:Nat), etc. to refer to this Chapter's version of
55
+
need to use explicit casts such as (0:Nat), (1:Nat), etc. to refer to this chapter's version of
56
56
the natural numbers.
57
57
-/
58
58
instance Nat.instOfNat {n:_root_.Nat} : OfNat Nat n where
···
90
90
-/
91
91
theorem Nat.succ_cancel {n m:Nat} (hnm: n++ = m++) : n = m := by
92
92
injection hnm
93
-
93
+
94
94
/--
95
95
Axiom 2.4 (Different natural numbers have different successors).
96
96
Compare with Mathlib's `Nat.succ_ne_succ`.
···
116
116
decide
117
117
118
118
/--
119
-
Axiom 2.5 (principle of mathematical induction). The `induction` (or `induction'`) tactic in
119
+
Axiom 2.5 (Principle of mathematical induction). The `induction` (or `induction'`) tactic in
120
120
Mathlib serves as a substitute for this axiom.
121
121
-/
122
122
theorem Nat.induction (P : Nat → Prop) (hbase : P 0) (hind : ∀ n, P n → P (n++)) :
+67
-49
analysis/Analysis/Section_2_2.lean
+67
-49
analysis/Analysis/Section_2_2.lean
···
2
2
import Analysis.Section_2_1
3
3
4
4
/-!
5
-
# Analysis I, Section 2.2
5
+
# Analysis I, Section 2.2: Addition
6
6
7
-
This file is a translation of Section 2.2 of Analysis I to Lean 4.
8
-
All numbering refers to the original text.
7
+
This file is a translation of Section 2.2 of Analysis I to Lean 4. All numbering refers to the
8
+
original text.
9
9
10
10
I have attempted to make the translation as faithful a paraphrasing as possible of the original
11
11
text. When there is a choice between a more idiomatic Lean solution and a more faithful
···
15
15
16
16
Main constructions and results of this section:
17
17
18
-
- Definition of addition and order for the "Chapter 2" natural numbers, `Chapter2.Nat`
19
-
- Establishment of basic properties of addition and order
18
+
- Definition of addition and order for the "Chapter 2" natural numbers, `Chapter2.Nat`.
19
+
- Establishment of basic properties of addition and order.
20
20
21
21
Note: at the end of this chapter, the `Chapter2.Nat` class will be deprecated in favor of the
22
22
standard Mathlib class `_root_.Nat`, or `ℕ`. However, we will develop the properties of
···
33
33
instance Nat.instAdd : Add Nat where
34
34
add := add
35
35
36
-
/-- Compare with Mathlib's `Nat.zero_add`-/
36
+
/-- Compare with Mathlib's `Nat.zero_add`. -/
37
37
@[simp]
38
38
theorem Nat.zero_add (m: Nat) : 0 + m = m := recurse_zero (fun _ sum ↦ sum++) _
39
39
40
-
/-- Compare with Mathlib's `Nat.succ_add` -/
40
+
/-- Compare with Mathlib's `Nat.succ_add`. -/
41
41
theorem Nat.succ_add (n m: Nat) : n++ + m = (n+m)++ := by rfl
42
42
43
-
/-- Compare with Mathlib's `Nat.one_add` -/
43
+
/-- Compare with Mathlib's `Nat.one_add`. -/
44
44
theorem Nat.one_add (m:Nat) : 1 + m = m++ := by
45
45
rw [show 1 = 0++ from rfl, succ_add, zero_add]
46
46
···
50
50
example : (2:Nat) + 3 = 5 := by
51
51
rw [Nat.two_add, show 3++=4 from rfl, show 4++=5 from rfl]
52
52
53
-
-- sum of two natural numbers is again a natural number
53
+
-- The sum of two natural numbers is again a natural number.
54
54
#check (fun (n m:Nat) ↦ n + m)
55
55
56
-
/-- Lemma 2.2.2 (n + 0 = n). Compare with Mathlib's `Nat.add_zero` -/
56
+
/-- Lemma 2.2.2 (n + 0 = n). Compare with Mathlib's `Nat.add_zero`. -/
57
57
@[simp]
58
58
lemma Nat.add_zero (n:Nat) : n + 0 = n := by
59
-
-- this proof is written to follow the structure of the original text.
59
+
-- This proof is written to follow the structure of the original text.
60
60
revert n; apply induction
61
61
. exact zero_add 0
62
62
intro n ih
···
64
64
(n++) + 0 = (n + 0)++ := by rfl
65
65
_ = n++ := by rw [ih]
66
66
67
-
/-- Lemma 2.2.3 (n+(m++) = (n+m)++). Compare with Mathlib's `Nat.add_succ` -/
67
+
/-- Lemma 2.2.3 (n+(m++) = (n+m)++). Compare with Mathlib's `Nat.add_succ`. -/
68
68
lemma Nat.add_succ (n m:Nat) : n + (m++) = (n + m)++ := by
69
69
-- this proof is written to follow the structure of the original text.
70
70
revert n; apply induction
···
88
88
rw [add_succ, ih]
89
89
90
90
/-- Proposition 2.2.5 (Addition is associative) / Exercise 2.2.1
91
-
Compare with Mathlib's `Nat.add_assoc` -/
91
+
Compare with Mathlib's `Nat.add_assoc`. -/
92
92
theorem Nat.add_assoc (a b c:Nat) : (a + b) + c = a + (b + c) := by
93
93
sorry
94
94
95
-
/-- Proposition 2.2.6 (Cancellation law)
96
-
Compare with Mathlib's `Nat.add_left_cancel` -/
95
+
/-- Proposition 2.2.6 (Cancellation law).
96
+
Compare with Mathlib's `Nat.add_left_cancel`. -/
97
97
theorem Nat.add_left_cancel (a b c:Nat) (habc: a + b = a + c) : b = c := by
98
-
-- this proof is written to follow the structure of the original text.
98
+
-- This proof is written to follow the structure of the original text.
99
99
revert a; apply induction
100
100
. intro hbc
101
101
rwa [zero_add, zero_add] at hbc
···
106
106
exact ih hbc
107
107
108
108
109
-
/-- (Not from textbook) Nat can be given the structure of a commutative additive monoid. -/
109
+
/-- (Not from textbook) Nat can be given the structure of a commutative additive monoid.
110
+
This permits tactics such as `abel` to apply to the Chapter 2 natural numbers. -/
110
111
instance Nat.addCommMonoid : AddCommMonoid Nat where
111
112
add_assoc := add_assoc
112
113
add_comm := add_comm
···
114
115
add_zero := add_zero
115
116
nsmul := nsmulRec
116
117
118
+
/-- This illustration of the `abel` tactic is not from the
119
+
textbook. -/
120
+
example (a b c d:ℕ) : (a+b)+(c+0+d) = (b+c)+(d+a) := by abel
121
+
117
122
/-- Definition 2.2.7 (Positive natural numbers).-/
118
123
def Nat.IsPos (n:Nat) : Prop := n ≠ 0
119
124
120
125
theorem Nat.isPos_iff (n:Nat) : n.IsPos ↔ n ≠ 0 := by rfl
121
126
122
127
/-- Proposition 2.2.8 (positive plus natural number is positive).
123
-
Compare with Mathlib's `Nat.add_pos_left` -/
128
+
Compare with Mathlib's `Nat.add_pos_left`. -/
124
129
theorem Nat.add_pos_left {a:Nat} (b:Nat) (ha: a.IsPos) : (a + b).IsPos := by
125
-
-- this proof is written to follow the structure of the original text.
130
+
-- This proof is written to follow the structure of the original text.
126
131
revert b; apply induction
127
132
. rwa [add_zero]
128
133
intro b hab
···
130
135
have : (a+b)++ ≠ 0 := succ_ne _
131
136
exact this
132
137
133
-
/-- Compare with Mathlib's `Nat.add_pos_right` -/
138
+
/-- Compare with Mathlib's `Nat.add_pos_right`. -/
134
139
theorem Nat.add_pos_right {a:Nat} (b:Nat) (ha: a.IsPos) : (b + a).IsPos := by
135
140
rw [add_comm]
136
141
exact add_pos_left _ ha
137
142
138
143
/-- Corollary 2.2.9 (if sum vanishes, then summands vanish).
139
-
Compare with Mathlib's `Nat.add_eq_zero` -/
144
+
Compare with Mathlib's `Nat.add_eq_zero`. -/
140
145
theorem Nat.add_eq_zero (a b:Nat) (hab: a + b = 0) : a = 0 ∧ b = 0 := by
141
-
-- this proof is written to follow the structure of the original text.
146
+
-- This proof is written to follow the structure of the original text.
142
147
by_contra h
143
148
simp only [not_and_or, ←ne_eq] at h
144
149
rcases h with ha | hb
···
150
155
contradiction
151
156
152
157
/-
153
-
The following API for ∃! may be useful for the next problem. Also, the `obtain` tactic is useful
154
-
for extracting witnesses from existential statements; for instance, `obtain ⟨ x, hx ⟩ := h`
158
+
The API in `Tools/ExistsUnique.Lean`, and the method `existsUnique_of_exists_of_unique` in
159
+
particular, may be useful for the next problem. Also, the `obtain` tactic is
160
+
useful for extracting witnesses from existential statements; for instance, `obtain ⟨ x, hx ⟩ := h`
155
161
extracts a witness `x` and a proof `hx : P x` of the property from a hypothesis `h : ∃ x, P x`.
156
162
-/
157
163
158
164
#check existsUnique_of_exists_of_unique
159
-
#check ExistsUnique.exists
160
-
#check ExistsUnique.unique
161
165
162
166
/-- Lemma 2.2.10 (unique predecessor) / Exercise 2.2.2 -/
163
167
lemma Nat.uniq_succ_eq (a:Nat) (ha: a.IsPos) : ∃! b, b++ = a := by
164
168
sorry
165
169
166
-
/-- Definition 2.2.11 (Ordering of the natural numbers)
170
+
/-- Definition 2.2.11 (Ordering of the natural numbers).
167
171
This defines the `≤` operation on the natural numbers. -/
168
172
instance Nat.instLE : LE Nat where
169
173
le n m := ∃ a:Nat, m = n + a
170
174
171
-
/-- Definition 2.2.11 (Ordering of the natural numbers)
175
+
/-- Definition 2.2.11 (Ordering of the natural numbers).
172
176
This defines the `<` notation on the natural numbers. -/
173
177
instance Nat.instLT : LT Nat where
174
178
lt n m := n ≤ m ∧ n ≠ m
···
177
181
178
182
lemma Nat.lt_iff (n m:Nat) : n < m ↔ (∃ a:Nat, m = n + a) ∧ n ≠ m := by rfl
179
183
180
-
/-- Compare with Mathlib's `ge_iff_le` -/
184
+
/-- Compare with Mathlib's `ge_iff_le`. -/
181
185
lemma Nat.ge_iff_le (n m:Nat) : n ≥ m ↔ m ≤ n := by rfl
182
186
183
-
/-- Compare with Mathlib's `gt_iff_lt` -/
187
+
/-- Compare with Mathlib's `gt_iff_lt`. -/
184
188
lemma Nat.gt_iff_lt (n m:Nat) : n > m ↔ m < n := by rfl
185
189
186
-
/-- Compare with Mathlib's `Nat.le_of_lt` -/
190
+
/-- Compare with Mathlib's `Nat.le_of_lt`. -/
187
191
lemma Nat.le_of_lt {n m:Nat} (hnm: n < m) : n ≤ m := hnm.1
188
192
189
-
/-- Compare with Mathlib's `Nat.le_iff_lt_or_eq` -/
193
+
/-- Compare with Mathlib's `Nat.le_iff_lt_or_eq`. -/
190
194
lemma Nat.le_iff_lt_or_eq (n m:Nat) : n ≤ m ↔ n < m ∨ n = m := by
191
195
rw [Nat.le_iff, Nat.lt_iff]
192
196
by_cases h : n = m
···
203
207
use 3
204
208
decide
205
209
206
-
/-- Compare with Mathlib's `Nat.lt_succ_self`-/
210
+
/-- Compare with Mathlib's `Nat.lt_succ_self`. -/
207
211
theorem Nat.succ_gt_self (n:Nat) : n++ > n := by
208
212
sorry
209
213
210
214
/-- Proposition 2.2.12 (Basic properties of order for natural numbers) / Exercise 2.2.3
211
215
212
-
(a) (Order is reflexive). Compare with Mathlib's `Nat.le_refl`-/
216
+
(a) (Order is reflexive). Compare with Mathlib's `Nat.le_refl`.-/
213
217
theorem Nat.ge_refl (a:Nat) : a ≥ a := by
214
218
sorry
215
219
216
220
/-- (b) (Order is transitive). The `obtain` tactic will be useful here.
217
-
Compare with Mathlib's `Nat.le_trans` -/
221
+
Compare with Mathlib's `Nat.le_trans`. -/
218
222
theorem Nat.ge_trans {a b c:Nat} (hab: a ≥ b) (hbc: b ≥ c) : a ≥ c := by
219
223
sorry
220
224
221
-
/-- (c) (Order is anti-symmetric). Compare with Mathlib's `Nat.le_antisymm` -/
225
+
/-- (c) (Order is anti-symmetric). Compare with Mathlib's `Nat.le_antisymm`. -/
222
226
theorem Nat.ge_antisymm {a b:Nat} (hab: a ≥ b) (hba: b ≥ a) : a = b := by
223
227
sorry
224
228
225
-
/-- (d) (Addition preserves order). Compare with Mathlib's `Nat.add_le_add_right` -/
229
+
/-- (d) (Addition preserves order). Compare with Mathlib's `Nat.add_le_add_right`. -/
226
230
theorem Nat.add_ge_add_right (a b c:Nat) : a ≥ b ↔ a + c ≥ b + c := by
227
231
sorry
228
232
229
-
/-- (d) (Addition preserves order). Compare with Mathlib's `Nat.add_le_add_left` -/
233
+
/-- (d) (Addition preserves order). Compare with Mathlib's `Nat.add_le_add_left`. -/
230
234
theorem Nat.add_ge_add_left (a b c:Nat) : a ≥ b ↔ c + a ≥ c + b := by
231
235
simp only [add_comm]
232
236
exact add_ge_add_right _ _ _
233
237
234
-
/-- (d) (Addition preserves order). Compare with Mathlib's `Nat.add_le_add_right` -/
238
+
/-- (d) (Addition preserves order). Compare with Mathlib's `Nat.add_le_add_right`. -/
235
239
theorem Nat.add_le_add_right (a b c:Nat) : a ≤ b ↔ a + c ≤ b + c := add_ge_add_right _ _ _
236
240
237
-
/-- (d) (Addition preserves order). Compare with Mathlib's `Nat.add_le_add_left` -/
241
+
/-- (d) (Addition preserves order). Compare with Mathlib's `Nat.add_le_add_left`. -/
238
242
theorem Nat.add_le_add_left (a b c:Nat) : a ≤ b ↔ c + a ≤ c + b := add_ge_add_left _ _ _
239
243
240
-
/-- (e) a < b iff a++ ≤ b. Compare with Mathlib's `Nat.succ_le_iff` -/
244
+
/-- (e) a < b iff a++ ≤ b. Compare with Mathlib's `Nat.succ_le_iff`. -/
241
245
theorem Nat.lt_iff_succ_le (a b:Nat) : a < b ↔ a++ ≤ b := by
242
246
sorry
243
247
···
262
266
263
267
264
268
/-- Proposition 2.2.13 (Trichotomy of order for natural numbers) / Exercise 2.2.4
265
-
Compare with Mathlib's `trichotomous` -/
269
+
Compare with Mathlib's `trichotomous`. -/
266
270
theorem Nat.trichotomous (a b:Nat) : a < b ∨ a = b ∨ a > b := by
267
-
-- this proof is written to follow the structure of the original text.
271
+
-- This proof is written to follow the structure of the original text.
268
272
revert a; apply induction
269
273
. have why : 0 ≤ b := by
270
274
sorry
···
287
291
followed by `exact Classical.decRel _`, but this would make this definition (as well as some
288
292
instances below) noncomputable.
289
293
290
-
Compare with Mathlib's `Nat.decLe`
294
+
Compare with Mathlib's `Nat.decLe`.
291
295
-/
292
296
def Nat.decLe : (a b : Nat) → Decidable (a ≤ b)
293
297
| 0, b => by
···
310
314
instance Nat.decidableRel : DecidableRel (· ≤ · : Nat → Nat → Prop) := Nat.decLe
311
315
312
316
313
-
/-- (Not from textbook) Nat has the structure of a linear ordering. -/
317
+
/-- (Not from textbook) Nat has the structure of a linear ordering. This allows for tactics
318
+
such as `order` to be applicable to the Chapter 2 natural numbers. -/
314
319
instance Nat.linearOrder : LinearOrder Nat where
315
320
le_refl := ge_refl
316
321
le_trans a b c hab hbc := ge_trans hbc hab
···
319
324
le_total := sorry
320
325
toDecidableLE := decidableRel
321
326
322
-
/-- (Not from textbook) Nat has the structure of an ordered monoid. -/
327
+
/-- This illustration of the `order` tactic is not from the
328
+
textbook. -/
329
+
example (a b c d:ℕ) (hab: a ≤ b) (hbc: b ≤ c) (hcd: c ≤ d)
330
+
(hda: d ≤ a) : a = c := by order
331
+
332
+
/-- (Not from textbook) Nat has the structure of an ordered monoid. This allows for tactics
333
+
such as `gcongr` to be applicable to the Chapter 2 natural numbers. -/
323
334
instance Nat.isOrderedAddMonoid : IsOrderedAddMonoid Nat where
324
335
add_le_add_left := by
325
336
intro a b hab c
326
337
exact (add_le_add_left a b c).mp hab
327
338
339
+
/-- This illustration of the `gcongr` tactic is not from the
340
+
textbook. -/
341
+
example (a b c d e:ℕ) (hab: a ≤ b) (hbc: b < c) (hde: d ≤ e) :
342
+
a+d < c + e := by
343
+
gcongr
344
+
order
345
+
328
346
/-- Proposition 2.2.14 (Strong principle of induction) / Exercise 2.2.5
329
-
Compare with Mathlib's `Nat.strong_induction_on`
347
+
Compare with Mathlib's `Nat.strong_induction_on`.
330
348
-/
331
349
theorem Nat.strong_induction {m₀:Nat} {P: Nat → Prop}
332
350
(hind: ∀ m, m ≥ m₀ → (∀ m', m₀ ≤ m' ∧ m' < m → P m') → P m) :
···
334
352
sorry
335
353
336
354
/-- Exercise 2.2.6 (backwards induction)
337
-
Compare with Mathlib's `Nat.decreasingInduction` -/
355
+
Compare with Mathlib's `Nat.decreasingInduction`. -/
338
356
theorem Nat.backwards_induction {n:Nat} {P: Nat → Prop}
339
357
(hind: ∀ m, P (m++) → P m) (hn: P n) :
340
358
∀ m, m ≤ n → P m := by
341
359
sorry
342
360
343
361
/-- Exercise 2.2.7 (induction from a starting point)
344
-
Compare with Mathlib's `Nat.le_induction` -/
362
+
Compare with Mathlib's `Nat.le_induction`. -/
345
363
theorem Nat.induction_from {n:Nat} {P: Nat → Prop} (hind: ∀ m, P m → P (m++)) :
346
364
P n → ∀ m, m ≥ n → P m := by
347
365
sorry
+9
-6
analysis/Analysis/Section_2_3.lean
+9
-6
analysis/Analysis/Section_2_3.lean
···
2
2
import Analysis.Section_2_2
3
3
4
4
/-!
5
-
# Analysis I, Section 2.3
5
+
# Analysis I, Section 2.3: Multiplication
6
6
7
-
This file is a translation of Section 2.3 of Analysis I to Lean 4.
8
-
All numbering refers to the original text.
7
+
This file is a translation of Section 2.3 of Analysis I to Lean 4. All numbering refers to the
8
+
original text.
9
9
10
10
I have attempted to make the translation as faithful a paraphrasing as possible of the original
11
11
text. When there is a choice between a more idiomatic Lean solution and a more faithful
···
16
16
Main constructions and results of this section:
17
17
18
18
- Definition of multiplication and exponentiation for the "Chapter 2" natural numbers,
19
-
`Chapter2.Nat`
19
+
`Chapter2.Nat`.
20
20
21
21
Note: at the end of this chapter, the `Chapter2.Nat` class will be deprecated in favor of the
22
22
standard Mathlib class `_root_.Nat`, or `ℕ`. However, we will develop the properties of
···
28
28
/-- Definition 2.3.1 (Multiplication of natural numbers) -/
29
29
abbrev Nat.mul (n m : Nat) : Nat := Nat.recurse (fun _ prod ↦ prod + m) 0 n
30
30
31
+
/-- This instance allows for the `*` notation to be used for natural number multiplication. -/
31
32
instance Nat.instMul : Mul Nat where
32
33
mul := mul
33
34
···
65
66
lemma Nat.pos_mul_pos {n m: Nat} (h₁: n.IsPos) (h₂: m.IsPos) : (n * m).IsPos := by
66
67
sorry
67
68
68
-
/-- Lemma 2.3.3 (Positive natural numbers have no zero divisors) / Exercise 2.3.2. Compare with Mathlib's Nat.mul_eq_zero. -/
69
+
/-- Lemma 2.3.3 (Positive natural numbers have no zero divisors) / Exercise 2.3.2.
70
+
Compare with Mathlib's `Nat.mul_eq_zero`. -/
69
71
lemma Nat.mul_eq_zero (n m: Nat) : n * m = 0 ↔ n = 0 ∨ m = 0 := by
70
72
sorry
71
73
···
87
89
theorem Nat.mul_assoc (a b c: Nat) : (a * b) * c = a * (b * c) := by
88
90
sorry
89
91
90
-
/-- (Not from textbook) Nat is a commutative semiring. -/
92
+
/-- (Not from textbook) Nat is a commutative semiring.
93
+
This allows tactics such as `ring` to apply to the Chapter 2 natural numbers. -/
91
94
instance Nat.instCommSemiring : CommSemiring Nat where
92
95
left_distrib := mul_add
93
96
right_distrib := add_mul