Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Errata chapters 6–10 plus tactics index #16

Open
wants to merge 52 commits into
base: main
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
52 commits
Select commit Hold shift + click to select a range
879abad
fix(4.1.4): grammar
dfpetrin Apr 27, 2024
e4a62ac
fix(4.2.3): grammar
dfpetrin Jan 3, 2024
885f232
fix(4.2.9): error in odd case
dfpetrin Apr 27, 2024
747a9c7
fix(6.1.2): mixed up integers and nats
dfpetrin Apr 29, 2024
9134de0
fix(6.1.5): add le 2 assumption to inductive step
dfpetrin Jan 7, 2024
c17e564
fix(6.2.5): use correct multiplication dot
dfpetrin Jan 7, 2024
0532915
fix(6.2.5): use n! instead of A_n
dfpetrin Jan 7, 2024
39252e3
fix(6.2.5): misnumbered case
dfpetrin Apr 28, 2024
7ccd6d5
fix(6.3.6): 6. match paper and lean statements
dfpetrin Jan 8, 2024
24d28a3
fix(6.4.2): use more accurate name for hypothesis
dfpetrin Jan 9, 2024
13f8831
fix(6.5.3): prove correct base cases
dfpetrin Jan 9, 2024
5fa02ed
fix(6.6.1): nitpick: use consistent n*d order
dfpetrin Jan 10, 2024
7b8cabe
fix(6.6.2): state inductive hyp with correct vars
dfpetrin Jan 10, 2024
778230c
fix(6.6.4): case 4 of proof missing a small step
dfpetrin May 3, 2024
33301ce
fix(6.7.1): remove unneeded hypothesis
dfpetrin Jan 11, 2024
8fac911
fix(6.7.3): state correct inductive hypothesis
dfpetrin Jan 11, 2024
43ad906
fix(6.7.3): typo
dfpetrin Apr 28, 2024
d61408b
fix(6.7.5): state correct inductive hypothesis
dfpetrin Jan 11, 2024
3eab70e
fix(6.7.5): fix minus sign
dfpetrin Jan 11, 2024
9f838e4
fix(7.3): use accurate hypothesis names
dfpetrin May 5, 2024
d79769d
refactor(7.3): simplify irrat_aux proof
dfpetrin May 5, 2024
a101b73
fix(7.3): minor typo
dfpetrin May 5, 2024
53dc5c2
fix(7.3): state and prove correct theorem
dfpetrin May 5, 2024
d213b30
fix(8.1.3): use consistent definition of `q`
dfpetrin May 6, 2024
a54bab2
fix(8.1.12): reference correct exercise
dfpetrin May 19, 2024
6a87991
fix(8.1.13): 17. real numbers -> rational numbers
dfpetrin May 18, 2024
a978548
fix(8.1.13): 17. fix lt_trichotomy statement
dfpetrin May 18, 2024
43fdb5b
fix(8.3.1): use correct definition of `comp`
dfpetrin May 21, 2024
ee3e08b
fix(8.3.10): 2. use rationals instead of reals
dfpetrin May 22, 2024
c694d54
fix(8.3.10): 5. use correct codomain for `g`
dfpetrin May 22, 2024
a509b41
fix(8.3.10) 7. typo
dfpetrin May 22, 2024
ba28571
fix(8.4.1): grammar
dfpetrin May 26, 2024
da8bea2
fix(8.4.8): use correct Id function
dfpetrin May 26, 2024
7786e6b
fix(8.4.9): fix the FIXME; use dsimp [i]
dfpetrin May 26, 2024
29f0f7d
fix(8.4.9): prove without using zify
dfpetrin May 26, 2024
a24bd04
fix(8.4.10): 8. use correct Id function
dfpetrin May 26, 2024
7eff382
fix(9.1.6): typo in proof
dfpetrin May 27, 2024
8e93a94
fix(9.1.8): case number typo
dfpetrin May 27, 2024
fab12d2
fix(9.1.9): typos in problem and proof
dfpetrin May 27, 2024
4e90bbb
fix(9.1.10): 10. typo in proof statement
dfpetrin May 27, 2024
99939e4
fix(9.2.3): use correct numeric type
dfpetrin May 27, 2024
fc0cba5
fix(9.2.5): use correct numeric type
dfpetrin May 27, 2024
0a9216a
fix(9.2.6): typos in problem statement
dfpetrin May 27, 2024
d9cf8db
fix(9.2.8): 2. use correct problem statement
dfpetrin May 27, 2024
fc8481c
fix(9.2.8): only first four use the tactic
dfpetrin May 27, 2024
8f1c696
fix(9.3.6): 2. nitpick: consistent sequence notation
dfpetrin May 29, 2024
a3beb0d
fix(10.1.1): typo in div not symm proof
dfpetrin May 29, 2024
0ebacd1
fix(10.1.1): typos in proof of div antisymm
dfpetrin May 29, 2024
2ffa6d8
fix(10.2.2): typo in proof
dfpetrin May 30, 2024
85611b4
fix(10.2.3): define equiv class more precisely
dfpetrin May 30, 2024
b34ec0e
fix(index): fix sorting
dfpetrin May 30, 2024
65a05fb
fix(index): add list of missing tactics/keywords
dfpetrin May 30, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
fix(6.7.5): state correct inductive hypothesis
  • Loading branch information
dfpetrin committed May 26, 2024
commit d61408be1de0ab4eb114a8f8d2b6fc8484623d62
5 changes: 3 additions & 2 deletions html/06_Induction.html
Original file line number Diff line number Diff line change
Expand Up @@ -2663,8 +2663,9 @@ <h3><span class="section-number">6.6.6. </span>Exercises<a class="headerlink" hr
<div class="admonition-proof admonition">
<p class="admonition-title">Proof</p>
<p>We prove this by strong induction on <span class="math notranslate nohighlight">\(b\)</span>. Suppose that for all
integers <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> with <span class="math notranslate nohighlight">\(|y|&lt;|b|\)</span>, it is true that
<span class="math notranslate nohighlight">\(0 \le \operatorname{gcd}(x, y)\)</span>.</p>
integers <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> with <span class="math notranslate nohighlight">\(|y|&lt;|b|\)</span>, it is true that</p>
<div class="math notranslate nohighlight">
\[L(x,y)x+R(x,y)y=\operatorname{gcd}(x,y).\]</div>
<p><strong>Case 1</strong> (<span class="math notranslate nohighlight">\(0&lt;b\)</span>): Let <span class="math notranslate nohighlight">\(q=\operatorname{div}(a,b)\)</span> and let
<span class="math notranslate nohighlight">\(r=\operatorname{mod}(a,b)\)</span>, so that <span class="math notranslate nohighlight">\(a=r+bq\)</span> (by <a class="reference internal" href="#mod-add-div"><span class="std std-numref">Example 6.6.2</span></a>).</p>
<p>Then by the recurrence definitions,</p>
Expand Down