Suggested approach: strong induction; start with a case split on the parity of \(n\),
using the lemma Nat.even_or_odd.
/- 5 points -/
+@[autograded 5]
theorem problem1 (n : ℕ) (hn : 0 < n) : ∃ a x, Odd x ∧ n = 2 ^ a * x := by
sorry
@@ -564,7 +564,7 @@
for all natural numbers \(a\) and \(b\), \(P_{a,b} =P_{b,a}\).
Suggested approach: well-founded induction, following the Lean template provided below.
(I have filled in everything except for the main inductive step.)
-/- 5 points -/
+@[autograded 5]
theorem problem2 (m n : ℕ) : pascal m n = pascal n m := by
match m, n with
| 0, 0 => rw [pascal]
@@ -589,11 +589,11 @@
\(\mathbb{R}\) is surjective.
(If you think it’s true, prove it, by solving the first version below. If you think it’s false,
solve the second version.)
-/- 4 points -/
+@[autograded 4]
theorem problem4a : Surjective (fun (x : ℝ) ↦ 2 * x) := by
sorry
-/- 4 points -/
+@[autograded 4]
theorem problem4b : ¬ Surjective (fun (x : ℝ) ↦ 2 * x) := by
sorry
@@ -603,11 +603,11 @@
\(\mathbb{Z}\) is surjective.
(If you think it’s true, prove it, by solving the first version below. If you think it’s false,
solve the second version.)
-/- 5 points -/
+@[autograded 5]
theorem problem5a : Surjective (fun (x : ℤ) ↦ 2 * x) := by
sorry
-/- 5 points -/
+@[autograded 5]
theorem problem5b : ¬ Surjective (fun (x : ℤ) ↦ 2 * x) := by
sorry
@@ -618,11 +618,11 @@
\(\mathbb{Q}\) is also injective.
(If you think it’s true, prove it, by solving the first version below. If you think it’s false,
solve the second version.)
-/- 5 points -/
+@[autograded 5]
theorem problem6a : ∀ (f : ℚ → ℚ), Injective f → Injective (fun x ↦ f x + 1) := by
sorry
-/- 5 points -/
+@[autograded 5]
theorem problem6b : ¬ ∀ (f : ℚ → ℚ), Injective f → Injective (fun x ↦ f x + 1) := by
sorry
diff --git a/searchindex.js b/searchindex.js
index b1582e36..ab288004 100644
--- a/searchindex.js
+++ b/searchindex.js
@@ -1 +1 @@
-Search.setIndex({docnames:["00_Introduction","01_Proofs_by_Calculation","02_Proofs_with_Structure","03_Parity_and_Divisibility","04_Proofs_with_Structure_II","05_Logic","06_Induction","07_Number_Theory","08_Functions","09_Sets","10_Relations","Homework","Index_of_Tactics","Mainstream_Lean","index","latexindex"],envversion:{"sphinx.domains.c":2,"sphinx.domains.changeset":1,"sphinx.domains.citation":1,"sphinx.domains.cpp":4,"sphinx.domains.index":1,"sphinx.domains.javascript":2,"sphinx.domains.math":2,"sphinx.domains.python":3,"sphinx.domains.rst":2,"sphinx.domains.std":2,sphinx:56},filenames:["00_Introduction.rst","01_Proofs_by_Calculation.rst","02_Proofs_with_Structure.rst","03_Parity_and_Divisibility.rst","04_Proofs_with_Structure_II.rst","05_Logic.rst","06_Induction.rst","07_Number_Theory.rst","08_Functions.rst","09_Sets.rst","10_Relations.rst","Homework.rst","Index_of_Tactics.rst","Mainstream_Lean.rst","index.rst","latexindex.rst"],objects:{},objnames:{},objtypes:{},terms:{"0":[1,2,3,4,5,6,7,8,9,10,14],"01_proofs_by_calcul":1,"02_proving_equalities_in_lean":1,"03_tips_and_trick":1,"1":[0,1,2,3,4,5,6,7,8,9,10,12,14],"10":[0,1,2,3,4,6,8,9,10,11],"100":[6,11],"10000":6,"1024":6,"104":3,"1048576":6,"1096":6,"10b":1,"10n":[4,8],"10t":1,"11":[1,2,3,4,6,9,11],"11n":3,"12":[2,3,4,8,12],"126":6,"12n":2,"13":[0,3,4,12],"14":[1,4],"15":[3,4,6],"16":[3,4,6,9],"16384":6,"1650":5,"17":[1,2,5,6],"1729":2,"1732":5,"18":[2,3,4,6],"19":4,"19349":6,"1960":1,"19684":5,"1cm":1,"2":[0,1,2,3,4,5,6,7,8,9,10,12,14],"20":[0,1,4,6,9],"2001":[0,1,14],"2013":0,"2014":1,"2022":0,"2023":0,"21":6,"2207":6,"23":11,"24":[3,4,6],"25":[0,2,12],"252":6,"256":6,"257":5,"26":[3,4],"267":6,"27":4,"28":5,"2a":[1,2,3,4,8],"2a_0":6,"2a_1":6,"2a_2":6,"2a_k":6,"2a_n":6,"2ab":1,"2an":1,"2anbm":1,"2b":[1,2,3,4,7,8],"2c":[1,8],"2f":8,"2k":[3,4,6,7,9],"2l":9,"2m":[1,6,8],"2n":[1,2,3,6,8,11],"2q":1,"2q_":6,"2r":2,"2r_":[6,11],"2s":[1,7,11],"2s_":6,"2t":3,"2t_":6,"2v":1,"2x":[1,2,3,4,6,8,11],"2x_1":8,"2x_2":8,"2x_k":6,"2x_n":6,"2xy":12,"2y":[1,2,3,8,9],"3":[0,1,2,3,4,5,6,7,8,9,10,12,14],"30":[4,5,11],"300":7,"31":6,"316837008400094222150776738483768236006420971486980607":6,"32":6,"33":11,"33m":11,"34":3,"35":6,"36":2,"38":11,"38n":11,"39":4,"3a":[2,3,4,8,10],"3ab":[1,2],"3b":[3,4],"3c":[1,10],"3c_n":6,"3d_":6,"3k":4,"3m":[2,3],"3n":[1,3,6,11],"3p":3,"3r":3,"3s":11,"3s_n":6,"3t":[1,2],"3u":1,"3w":1,"3x":[2,8,9,11],"3y":[1,3,4,8],"3z":8,"4":[0,1,2,3,4,5,6,7,8,9,10,12,14],"40":[3,4,9],"4096":6,"42":9,"4294967297":5,"45":4,"450":7,"46":2,"4623":6,"47":6,"49":2,"4a":[1,3,9,11],"4ab":1,"4anbm":1,"4b":[1,4],"4c_n":6,"4k":[6,9],"4m":2,"4n":[2,4,9],"4q":[1,11],"4u":1,"4x":[1,4],"4y":3,"5":[0,1,2,3,4,5,6,7,8,9,10,12,14],"50":[3,10],"55":0,"56":6,"59":6,"5a":[1,3,4,9],"5b":[1,2,4],"5b_":[6,11],"5d_k":6,"5d_n":6,"5k":[9,11],"5m":8,"5m_1":8,"5m_2":8,"5n":[1,3,4,9,11],"5q":4,"5s":3,"5t":[2,9],"5x":[1,3,8],"6":[0,1,2,3,4,5,6,7,8,9,14],"628":1,"63":[3,4],"64":6,"641":5,"65":3,"65537":5,"66":11,"6700417":5,"69":2,"6a":[1,3],"6b_n":[6,11],"6k":9,"6n":6,"6p_":6,"7":[0,1,2,3,4,5,6,7,8,9,10,14],"70":6,"72":1,"75":0,"79":[4,11],"7b":1,"7n":[3,9],"7t":1,"8":[0,1,2,3,4,5,6,7,8,9,14],"80":0,"84":2,"85":2,"88":3,"8a":[1,3,4,9],"8b":[1,3],"8n":8,"8n_1":8,"8n_2":8,"8x":[1,11],"9":[0,1,2,3,4,6,8,9,10,11],"97":[4,11],"9k":9,"\u03b1":[2,5,9,10,11],"\u03b2":[5,10],"\u03b3":10,"\u1d9c":9,"\u2115":[2,3,4,5,6,7,8,9,10,11],"\u211a":[1,2,4,6,8,9,11],"\u211d":[1,2,4,5,6,8,9,10,11],"\u2124":[1,2,3,4,5,6,7,8,9,10,11],"abstract":[5,8,10,13],"b\u00e9zout":[7,14,15],"break":[0,2,4,7,8],"case":[0,1,3,4,5,6,7,8,9,10,11,12,14,15],"class":[0,3,4,5,10],"default":3,"do":[0,1,2,3,4,5,6,7,8,11,13],"final":[0,1,2,4,5,7,8,12],"function":[0,3,9,10,11,14,15],"gr\u00f6bner":13,"hq\u2081":4,"hq\u2082":4,"import":[1,2,3,4,5,6,10],"int":[3,4,6,9,10,11,13],"long":[1,2,4,5,6],"mul_left_cancel\u2080":13,"new":[0,1,2,3,4,6,8,9,12],"return":[5,10],"short":[0,1,6],"switch":6,"throw":[0,3],"true":[0,2,3,4,5,6,8,9,10,11,12],"try":[1,2,3,5,6,8,10],"while":[1,5,12],A:[0,2,3,4,5,6,7,8,9,10,12,13,14,15],And:[1,3,5,6,8,9,14,15],As:[1,2,3,4,5,6,8],At:[0,1,2,4,5,6,8,9],Be:1,But:[0,1,2,3,4,5,6,7,8,9],By:[2,4,5,6,7,8,9,10],For:[0,1,2,3,5,6,7,8,9,10,14,15],If:[0,1,2,3,5,6,7,8,9,10,11,12,13,14,15],In:[0,1,2,3,4,5,6,7,8,9,10,13],Is:5,It:[0,1,2,3,4,5,6,7,9,10,11],No:2,On:[1,2,3,9],One:[1,2,4],Or:[3,7,14,15],Such:[3,8],That:[1,2,3,4,5,6,7,9],The:[0,1,2,3,4,8,10,11,13,15],Then:[1,2,3,4,5,6,7,8,9,10],There:[0,1,2,3,5,6,7,8,9,14,15],These:[0,2,4,5,6,7,8,13,14],To:[1,2,4,5,6,7,8,9,13],With:[6,12],_:[1,2,3,4,5,6,7,8,9,10,11],_x:8,_y:8,a1:[8,10],a2:[8,10],a_0:6,a_1:[6,10],a_2:[6,10],a_3:6,a_4:6,a_5:6,a_:[6,8],a_k:6,a_m:6,a_mono:8,a_n:[6,8],ab:[1,2,3,5,7,11],abl:[1,3,12],about:[1,2,3,4,5,6,7,8,9,14,15],abov:[1,2,3,4,5,6,7,8,9],abs_le_of_sq_le_sq:[2,4],absolut:6,abus:0,ac:3,accept:1,access:2,accord:[3,4,6,8,9,12],accordingli:4,account:1,acknowledg:[14,15],acronym:6,act:2,actual:[0,1,2,3,4,7],ad:[1,2,6,10,13],adapt:[1,2,5,6,8,9],add:[0,1,2,3],addarith:[1,2,4,6,7,8,9,12,13],addit:[1,2,5,8,12],adjust:13,adopt:0,advanc:[1,6],advantag:1,aesop:13,af:[1,10],after:[0,1,2,3,4,5,6,8,9,10,12,13],afterward:2,again:[1,2,3,6,7,9],agre:[5,6],aim:14,air:8,ak:[3,10],aka:0,algebra:[0,1,2,6,12,13],algorithm:[0,11,14,15],all:[0,1,2,3,5,6,7,8,9,10,11,13,14,15],allow:[1,2,4,5],almost:[0,1,6],alon:[1,6],along:[2,6,10],aloud:0,alpha:10,alreadi:[0,1,2,3,4,5],also:[0,1,2,3,4,5,6,7,8,9,10,11],altern:[0,2,3,8,9,12],although:[2,3,5,6],alwai:[5,6,7,13],am:[1,10],ambigu:7,ami:10,amount:[0,6,9],an:[0,1,2,3,4,5,6,7,8,9,10,11,12,13],analogu:6,analysi:[0,8],analyz:4,ancient:[5,7],angl:4,ani:[0,2,3,4,5,6,8,10,11,13],annot:[0,1,4],announc:2,anoth:[1,2,3,4,5,6,7,8,9,10,13],answer:9,anteced:[4,12],antisymmetr:[14,15],antisymmetri:2,anyth:[4,5],anywai:2,anywher:1,apart:[2,12],appar:6,appear:[0,1,2,3,4,11],appendic:14,appendix:[0,13],appli:[1,2,3,4,5,6,7,8,9,10,11,12],applic:[2,6],appris:0,approach:[1,6,8,9,11],appropri:1,approxim:4,ar:[0,1,2,3,4,5,6,7,8,9,10,11,12,13,14],arami:8,arbitrari:[4,8],arg:10,argument:[0,1,2,4,6,7],aris:8,arithmet:[4,6,11,12,14,15],around:[1,9],arrow:7,ask:[1,2,4,6,12],assess:0,assign:0,assist:[0,1],associ:[1,13,14],assum:[1,2,4,8,12],assumpt:[5,8,9],atho:8,atom:0,attempt:[6,12],attent:0,attribut:6,author:14,auto:0,autom:[0,8],automat:[0,1,5,6],av:1,avail:[0,2,3,4,6,7,12],avigad:0,avoid:[0,1,6,7,13],awai:5,awar:13,awkward:5,ax:[3,6,11],axiom:[5,8],b1:8,b2:8,b:[1,2,3,4,5,6,7,8,9,10,11,13],b_0:[6,11],b_1:[6,11],b_2:6,b_3:6,b_:[6,11],b_k:6,b_n:[6,11],ba:1,back:[0,1,2,3,5,7],background:0,backward:[0,6],banana:2,barber:9,base:[0,6,7,13],basic:[0,5,6,13],bc:[1,7],bd:3,becaus:[0,2,4,5,6,8,13],becom:[0,2,6,8,12],been:[0,1,2,4,5,6,8,14],befor:[1,2,3,4,5,6,8],begin:[1,2,4,5,6,7],beginn:1,behaviour:[2,10],behind:9,being:[0,1,2,3,6,9,10],believ:6,belong:9,below:[2,4,6,8,9,11],ben:2,bernoulli:6,best:13,beta:10,beth:10,better:[3,4,6,7,8,9,13],better_prime_test:[4,5,11],between:[0,2,3,4,5,6,7,11],beyond:[0,8,13],bezout:[6,7],bi:[4,10],big:[0,1,2],biject:[10,14,15],bijective_iff_exists_invers:[8,10],bijective_of_invers:8,bilingu:0,bit:[4,5,6],bk:4,bl:10,blackboard:[0,4],block:[0,1,2,6,13],blue:1,bm:1,bn:[1,10],board:13,book:[1,2,3,4,5,6,7,8,9,12,14,15],both:[0,1,2,3,4,5,6,8,9,12],bottom:[1,2],bound:[1,4,6,12],bq:[3,4,6,11],brahmagupta:[1,7],branch:9,breakdown:0,breather:3,brief:0,bring:3,broader:8,broken:2,brought:[2,5],brown:5,build:[0,1,9],built:[2,3,4,6],bundl:6,bv:1,by_cas:[5,6,8,9,11,12],byd:7,c:[1,2,3,4,6,7,8,9,10,11,13],c_0:6,c_1:6,c_:6,c_n:6,ca:1,cab:2,calc:[1,2,3,4,5,6,7,8,9,10,11],calcul:[0,2,5,6,7,13,14,15],calculu:0,call:[0,1,2,4,5,6,7,9],came:1,can:[0,1,2,3,4,5,6,7,8,9,10,11,13],cancel:[0,1,2,3,4,6,7,8,10,11,12,13],candid:8,cannot:[1,4,7],canon:[0,6],cap:9,capabl:[6,8,13],capston:7,care:[0,14],carefulli:[1,4,12],carneiro:0,carri:[0,1,2,7,9,13],cast:[1,7],casual:2,caus:[1,2],caveat:5,cb:[1,10],cdot:[1,2,3,4,5,6,7,8,9,10,11,12],ce:1,celesti:8,central:[5,7],certain:[0,2,9,13],certainli:[1,5],cf:[1,10],chain:1,chanc:3,chang:[0,2,6],chapter:[0,1,2,3,4,5,6,7,8,9,10],character:[4,6],characteris:4,check:[1,2,3,4,5,6,8,9,11,12,13],check_equality_of_explicit_set:9,checkabl:8,choic:[0,4,8],choler:8,choos:[1,2,8],chosen:2,circ:8,circl:7,circul:0,circular:6,claim:[4,7],classic:[0,1,2],classroom:0,claus:6,clean:9,clear:[2,6],clearer:4,clearli:[0,4,5,8],clever:[1,2,7],click:3,cliqu:10,close:[1,4,6,7,8],closer:2,cloud:[0,1,14],co:8,code:[0,1,2,3,13,14],codespac:0,codomain:8,coeffici:1,collect:[9,13],colloqui:4,colon:1,colour:10,com:[1,14],combin:[0,1,3,4,5,6,8,9,10,13],come:[0,1,2,3,8],comfort:0,command:[3,5,8],comment:14,commentari:0,common:[1,2,4,6,7,8,12],commonli:[0,1,2],commun:[0,13],comp:[8,10],compact:3,compar:[2,4,5,6,8,9,11,12],comparison:[1,12],complain:1,complement:9,complet:[0,2,6],complex:[2,5,8],complic:[0,1,2,4,6,8],compon:8,compos:5,composit:[14,15],comprehens:[0,5],comput:[0,1,5,6,14],concept:[0,2,3,4,5,9],conceptu:[5,8],concern:3,concis:1,conclud:[0,1,2,4,6,7,8,12],conclus:[1,2,4,7],concret:[5,6],condit:2,confirm:[2,8,9],confus:3,congruenc:[3,4,6,12],congruent:[3,4,6,10,11],connect:[0,1,2,4,10],consecut:[3,4,7],consequ:2,consid:[1,2,3,4,5,6,7,8,9,10,11],consider:2,consist:[1,2,7,8,10],consolid:3,constant:[1,6,13],constitu:2,constitut:[0,7,8],constrain:0,construct:[6,8],constructor:[2,3,4,5,6,7,8,9,10,12],consult:[1,12],contain:[0,1,2,4,7,8,9,13],context:[3,8,9],continu:[0,2,6],contradict:[5,6,7,8,9,12,14,15],contradictori:[8,12,14,15],contraposit:5,contribut:5,conv:[5,9],conveni:[3,4,5,6,8,9,10],convent:[0,2,6],convers:[0,4,8,9,10],convert:[4,5,7,8,11,12],copi:2,core:0,corollari:8,correct:[0,1,3,9,14],correctli:9,correspond:[0,1,2,3,7],could:[1,3,4,7,8],counteract:1,coupl:4,cours:[0,4,5,13,14],courteou:1,cover:[0,1,2,3,5,13],creat:[1,2,4,8],creativ:2,credit:[6,11],crucial:3,ctrl:3,cube:2,cup:9,current:[0,2,3,6],cursor:2,curv:0,custom:0,cx:8,d:[1,2,3,6,7,10],d_0:6,d_1:6,d_4:6,d_5:6,d_:6,d_k:6,d_n:6,dagger:7,dai:0,danger:6,date:7,david:0,davidson:2,dbe:1,de:[1,5],deal:[0,1,2,3,14],dealt:8,debt:4,decidableeq:[8,10],decim:6,decreas:[6,7],deduc:[1,2,4,5,6,11],deduct:[0,1,2,4,12],deeper:5,def:[3,4,5,6,8,9,10,11],defin:[0,4,7,8,9,10,11],definit:[0,2,11,12,14,15],degre:1,delai:5,delet:[2,3,12],deliber:13,delic:[1,6],demonstr:5,denot:[2,3,6,7,8,9,10],depart:0,depend:[1,3,4,5,6,11],deriv:[4,8,10],describ:[6,8,9],descript:9,design:[0,1,9],desir:[2,4,5,6,9],detail:[0,2,3,6,13],determin:[1,2,10],develop:[0,1,6,7],devot:0,dialect:[0,13],did:[2,4,5,8],differ:[0,1,2,3,4,6,7,8,9,10,12,13],difficult:[2,7,8],difficulti:1,direct:[1,4,5,6,8,10],direction:10,directli:[1,2,3,4,6,9,11],discov:[1,13],discoveri:[5,13],discret:6,discuss:[1,2,3,4,8,9,13],disequ:2,disguis:9,displai:[2,3,6,7,8,9],disprov:[8,9,11],distinct:2,distinguish:0,div:6,divid:[1,3,6,11],divis:[0,1,2,5,7,8,11,13,14,15],divisor:[3,6,7,8],dk:7,dl:7,document:13,doe:[0,3,4,5,6,8,9,11,13],doesn:[1,4,5,8],domain:8,don:[0,1,2,3,4,5,6,8,9,11],done:[1,2,3,4,5,6,7,8,10,13],dot:3,doubl:[1,3],down:[1,2,6,7,8,9],download:[1,14],draw:[1,2,7,10],dream:0,drop:[0,1],dry:10,dsimp:[3,4,5,6,7,8,9,10,11,12],due:6,dull:2,durat:3,dvd:3,dvd_factori:[6,7],dvd_iff_modeq:4,dx:6,dy:6,dz:7,e:[1,3,8,10],each:[0,1,2,4,5,6,8,9,10,12],earli:[0,2,8,14],earlier:[2,4,5],earth:8,easi:[0,1,2,3,6,13],easier:[0,2,4],easili:[0,1,4],eb:10,ebner:0,ed:10,edmond:5,effect:[2,3,8,12],effici:[0,4,8,13],effort:0,either:[1,2,3,4,5,6,7,8,9,11],electron:8,eleg:6,element:[7,8,9,10],elementari:[0,3,6],elimin:[1,13],els:[2,6,10],elsewher:[0,1,8],email:0,emphasi:6,empti:9,emptyset:9,enclos:6,encount:[0,3,4,5,6],end:[1,2,5,6,13],endgam:6,endless:0,enforc:0,english:[0,2],enjoi:[0,13],enough:[0,2,3,6,8],ensu:8,ensur:0,enthusiasm:0,enthusiast:0,environ:[0,1],eq_of_rel:10,eq_or_lt_of_l:[4,6],eq_zero_or_eq_zero_of_mul_eq_zero:[2,4,11],eq_zero_or_po:10,equal:[0,2,4,5,6,7,8,9,12,14,15],equat:[1,2,4,5,8],equiv:[3,4,6,8,9,10,11],equival:[0,7,8,9,11,12,14,15],equivalenceclass:10,erron:1,error:[0,1,6],especi:0,establish:[0,1,2,4,6,7],etc:[1,2,4,6,7,11,12,13],euclid:[0,14,15],euclid_lemma:7,euclid_lemma_pow:7,euclidean:[11,14,15],euler:5,eval:[6,8],evalu:6,even:[0,1,3,4,5,6,7,8,9,11],even_iff_modeq:4,even_iff_not_odd:[4,9],even_of_pow_even:[6,7],even_or_odd:[3,4,6,11],eventu:6,everi:[1,2,3,4,5,6,8,9,10],everyth:[0,7,8,9,11],everywher:3,exact:[6,13],exactli:[1,2,3,4,6],exam:7,examin:0,exampl:[0,7,11,13],except:[2,11],exclud:[11,14,15],exercis:[0,7,11],exhaust:8,exist:[0,3,5,6,7,8,9,10,11,12,13,14,15],existenti:[0,2,3,12],exists_factor_of_not_prim:[5,6],exists_inverse_of_biject:8,exists_prime_factor:[6,7],existsunique_modeq_lt:[4,6],exot:6,expand:[1,8,12],expect:[0,2,8,13],experi:[0,1,6],experienc:0,experiment:0,expert:[0,5,8],explain:[0,1,2,6,9],explan:6,explicit:[1,6,8],explicitli:[0,1,2,4,7,9],exploit:1,explor:[7,13],expon:6,exponenti:12,express:[0,1,2,3,4,6,9],ext:[8,9,10],extend:[6,11],extens:1,extension:[8,9],extra:[0,1,2,3,4,6,7,8,9,12,13],extract_pow_two:6,extrem:[7,13],ey:1,f1:10,f2:10,f:[1,6,8,9,10,11],f_0:6,f_1:6,f_1f_0:6,f_:6,f_bound:6,f_k:6,f_m:6,f_n:6,facil:6,fact:[0,1,2,3,4,5,6,7,8,10,12],factor:[2,3,4,5,6,7,12],factori:[6,7],factorial_po:[6,7],fail:[1,2,5],fairli:[0,5,6,8],fall:0,fals:[0,4,5,8,9,10,11,12],falsehood:5,famili:[5,6],familiar:[0,1,2,9],famou:[5,6,7],far:[1,2,6,7,8,12],fdiv:6,featur:[0,1,2,3,4,6,9,13],feedback:[0,1],feel:[1,2,3,4],fermat:5,few:[0,1,6,13],fewer:[0,6],fibonacci:[6,8],fiddli:7,field_simp:6,fifti:0,figur:2,file:[0,1],fill:[0,1,2,4,6,8,11],find:[0,2,3,4,5,6,7,8,11,13],fine:[1,7,8],finger:3,finish:[2,4,8],finit:[4,6,8,9,10],fire:8,first:[0,1,2,3,4,5,6,7,8,9,10,11,12,13],firstli:[4,8],five:[1,9],fix:[5,6],fixm:8,flatter:0,flexibl:[0,1,6,8],fluenci:0,fmod:6,fmod_add_fdiv:6,fmod_lt_of_po:6,fmod_nonneg_of_po:6,focu:[0,1],follow:[1,2,3,4,5,6,7,8,9,10,11,12],foo:2,footnot:[0,1,2,3,4,5,6,8,9],foral:[4,5,9,11,12],forall_sufficiently_larg:[4,6,11],fordham:[0,2,14],foreign:0,forev:6,form:[1,2,4,6,7,8,10,12,14,15],formal:[0,1,3,4,5,13,14],former:[4,9],formul:9,formula:[4,5,6,8],forth:0,fortun:8,forum:12,forward:0,found:[0,6,7,11],foundat:9,founded:[0,6,7],four:[1,8],four_not_prim:5,four_prim:5,fourier:13,fourth:1,frac:[1,2,3,4,5,6,8,11],frankli:8,free:[0,4,8,11],frequent:[3,6],from:[0,1,2,3,4,5,6,7,8,9,11,12,13],front:1,full:[1,2,3,5,6,8,9,13],fulli:[0,2],fun:[7,8,10,11,13],fundament:[4,7],further:[1,2,8,13],furthermor:1,fussi:0,futur:[0,2,4,5,6,8],g1:8,g2:8,g:[2,8,10],g_1:8,g_2:8,gabriel:0,game:5,gauss:[14,15],gauss_lemma:7,gcd:[6,7,11],gcd_dvd:6,gcd_dvd_left:[6,7],gcd_dvd_right:[6,7],gcd_maxim:6,gcd_nonneg:[6,7],gcongr:13,ge:[1,2,4,6,9,11],gener:[1,2,3,4,5,6,7,8,9,13],geq:[1,2,3,4,5,6,7,9,11],get:[0,1,2,4,6,8,11,12],github:[0,1,14],gitpod:[0,1,14],give:[1,2,3,4,5,6,7,8],given:[1,2,3,4,6,7,8,9,10,12],go:[0,1,2,3,8],goal:[0,1,2,3,4,5,6,8,9,12],goe:[5,6,9],good:[0,5,8],googl:12,grade:0,grader:0,gradescop:[0,11],gradual:2,grammar:[4,5],grant:[0,3],graph:10,great:3,greater:[1,2,4,6,7,11],greatest:[6,7,8],greedili:1,greek:[0,5,7],grew:0,group:0,guarante:7,guardrail:0,guess:[3,10,13],h0:8,h1:[1,2,3,4,5,6,7,8,9,10,11],h1m:4,h2:[1,2,3,4,5,6,7,8,9,10,11],h3:[1,2,4,5,6,9],h4:[1,2,4,6],h5:[1,4],h6:[1,9],h7:1,h8:1,h9:1,h:[1,2,3,4,5,6,7,8,9,10,11],h_div:4,h_gauss:7,h_gt:7,h_inj:8,h_le:7,h_moon:8,h_pyth:4,h_refl:10,h_sun:8,h_surj:8,h_symm:10,h_tran:10,ha1:4,ha1b:10,ha2:4,ha2b:10,ha:[0,1,2,3,4,5,6,7,8,9,10,11,13],hab:[2,3,4,6,7,8,10,11],hack:0,had:[0,1,2,4,9],half:[4,5],halfwai:[0,1],hammack:[2,3,6],hand:[1,2,4,5,6,8,10,12,13],handl:[7,8,13],handwritten:4,hap1:7,hap2:7,happen:[1,2,4,5,6],hard:[0,2,3,6,8,11],harder:[2,4],hardi:2,hardli:5,hasn:5,hat:8,haunt:0,have:[0,1,2,3,4,5,6,7,8,9,10,11,12,13,14],haven:[2,7],hb1:4,hb2:4,hb:[2,3,4,6,7,8],hbc:[3,10,11],hbk:7,hc:[2,4],hd:[6,7],he:2,head:[1,3,5,14],heartfelt:0,heather:14,heavi:0,help:[1,2,6,12,13],henc:[6,7,8],henceforth:8,here:[0,1,2,3,4,5,6,7,8,9],herself:2,hertz:0,hf1a:10,hf1b:10,hf2a:10,hf2b:10,hf:[8,9,10],hfact:4,hfg1:10,hfg2:10,hfg:8,hfx:9,hg:8,hgcd:7,hgcd_1:7,hgcd_p:7,hgf:8,hi:[2,8],high:[0,1,2,4],him:2,himself:9,hk1:[4,5,6],hk:[3,4,5,6,7,8,9,10],hkl:4,hkp:[4,5],hl1:4,hl2:4,hl:[4,6,7,9,10],hm1:[4,8],hm2:[4,8],hm:[2,3,4,6,8],hm_left:4,hm_right:4,hmn:6,hmp:4,hmp_le:4,hmt:4,hn0:[2,7],hn1:4,hn2:[4,6,7],hn:[1,2,3,4,5,6,8,9,11],hneg:4,hold:[5,7,9,10],homework:[0,4,7,14],honest:0,honestli:1,hood:4,hope:[0,2],hopefulli:4,horizon:8,horizont:1,hour:0,hover:3,how:[0,1,2,3,4,5,6,8,9,13,14],howev:[6,8],hp1:7,hp2:[5,7],hp:[2,3,4,5,6,7],hpn:7,hpo:4,hpq:[3,5],hq:[3,5],hqr:3,hr1:4,hr2:4,hr3:4,hr:[3,4,6],hrmacbeth:[1,14],hs:[3,6,9],hspace:1,hst:9,ht:[1,2,7,9,11],htp:4,http:[1,14],human:[1,2,6],humour:8,hundr:0,hx1:[8,9],hx1x2:8,hx2:[8,9],hx:[1,2,3,4,5,6,8,9,10,11],hxt:2,hxx1:8,hxx2:8,hxy:10,hy:[1,2,3,4,6,8,10],hyperlink:13,hypothes:[0,1,2,3,6,7,8,12,13,14,15],hypothesi:[1,2,3,4,6,7,8,12],hyz:10,hz:7,i:[0,1,2,3,4,5,6,8,9,11,13],id:[1,8,10],idea:[1,4,5,6,7,8,9,11],ident:[1,7,8,14,15],identifi:2,idiomat:0,ignor:1,ih1:6,ih2:6,ih:[6,7,8],ih_left:6,ih_right:6,ii:[0,2,9,14,15],ill:2,imag:6,imagin:5,immedi:[1,2,4,6,8],imo:1,implement:0,impli:[1,2,4,10],implic:[12,14,15],implicitli:[0,1,4,6],importantli:1,imposs:[0,4,7],improv:6,incant:9,includ:[0,2,4,8,9,10,11,13],incorrect:1,increasingli:[0,6],inde:[2,3,4,5,6,7,8,9,10],independ:[2,13],index:[6,8,14,15],indian:1,indic:[1,2,6,9,11,12],individu:[0,1],induct:[0,7,8,10,11,13,14,15],induction_from_starting_point:[6,7,8,13],inequ:[0,2,4,5,6,12,13,14,15],infer:[1,9],infinit:[4,14,15],infinitud:0,infix:10,inform:[0,1,4,5,9],infoview:[1,2,6,7,8,9],infrastructur:0,ingredi:2,initi:[1,2,3],inject:[9,10,11,14,15],input:[6,7,8],insert:4,insid:[0,1,3,5],inspect:[2,8,12],instal:[0,1],instant:[0,1],instanti:6,instead:[0,1,2,4,5,7,8,11],instruct:[0,1],instructor:[12,14,15],integ:[0,1,2,3,4,6,7,8,9,10,11,12],intellectu:0,interact:[0,1,2,7,13],interest:[0,1,2,3,6],intermedi:[1,3,5,14,15],intern:13,internet:12,interpret:1,intersect:9,intertwin:8,interval_cas:[4,6,9,12],interview:0,intrepid:0,intro:[0,4,5,6,7,8,9,10,12],introduc:[0,1,2,3,4,5,6,7,8,9,10,12],introduct:[4,14,15],intuit:[5,8],invers:[8,10],invis:2,invoc:8,invok:[0,1,3,4,6,7,8,9,12,13,14,15],involv:[1,2,4,5,6,8],inward:[5,12],irrat:[5,7],irrat_aux:7,irrat_aux_wf:7,irration:0,isn:1,issu:[6,13],iter:[0,9],its:[1,2,3,4,5,6,7,8,9,10,12,13],itself:[2,6,8,9],j:4,jack:8,jeremi:0,jo:10,joint:6,jointli:6,joseph:5,just:[0,1,2,3,4,5,6,7,8,9,10,11],justif:[0,1,2,4,6,7],justifi:[1,2,6],juxtapos:0,k:[3,4,5,6,7,8,9,10,11],k_contra:7,keep:[0,2,6],kei:[1,2,7],kept:0,keyboard:3,keyword:[1,2],kind:[1,3,4,5,6,7,8,13],kl:[4,10],knock:9,know:[0,1,5,6,7,10],knowledg:[0,2],known:[0,1,2,4,5,6,7],kq:6,ky:6,l01:0,l:[3,4,5,6,7,8,9,10],l_mul_add_r_mul:6,label:4,land:[2,4,5,9,11,12],languag:[0,2,9,10,14],larg:[4,6,11],larger:[2,4,6],last:[1,2,3,5,6,8,9],later:[0,1,2,3,4,6,7],latter:[4,9],law:[2,11,14,15],ldot:[1,2,4,6],le:[1,2,3,4,5,6,7,8,9,10,11],le_add_of_nonneg_right:13,le_antisymm:[2,4,6,8,10,11],le_induct:13,le_of_dvd:[3,4,10],le_of_pow_le_pow:0,le_or_gt:2,le_or_lt:[4,7,8,9],le_or_succ_l:[2,4,5,11],lead:6,lean:[2,3,4,5,6,7,8,9,11,14,15],learn:[0,1,2,3,4,5,6],least:[2,3,4,9],leav:[1,2,4,5,8],lectur:[0,2,4,7,12,14],led:1,left:[0,1,2,4,5,6,7,8,9,10,12],leftarrow:4,leftrightarrow:[4,5],lemma:[0,6,8,11,12,13,14,15],leonardo:1,leonhard:5,leq:[1,2,4,10],less:[2,3,4,10],let:[0,1,2,3,4,5,6,7,8,9,10,11],level:[0,6,8,10,13,14],lewi:0,lh:12,li:[3,4,7,11],liber:9,librari:[0,1,2,3,4,5,13],life:2,lift:7,lightli:0,like:[0,1,2,3,4,5,6,7,8,9,12],likewis:[1,4,5,6,10],limit:[0,6],linarith:13,line:[1,2,3,4,5,6,8,9,10,11,12,13],linear:13,link:0,list:[2,4,6,9],literatur:13,littl:[2,6,10],live:[0,1,2],ll:[1,2,3,5,8],lnot:[4,5,11,12],local:10,logic:[0,2,3,4,6,7,8,9,11,12,13,14,15],longer:[0,2],look:[0,1,2,3,4,5,6,9,12],lor:[2,3,4,5,9,11,12],lose:0,lot:[3,8],low:6,lower:[6,12],lower_bound_fmod1:6,lower_bound_fmod2:6,lt:2,lt_add_of_pos_right:13,lt_fmod_of_neg:6,lt_of_le_of_n:6,lt_of_pow_lt_pow:13,lt_or_l:4,lt_trichotomi:8,luck:13,lx:7,ly:2,m1:8,m2:8,m:[1,2,3,4,5,6,8,9,10,11],m_1:8,m_2:8,mac:3,macbeth:14,macro:9,made:10,magic:1,mai:[0,1,2,3,4,6,8,9,13],main:[0,2,3,6,7,11],mainstream:[0,14,15],major:[0,3,13],make:[0,1,2,3,4,5,6,7,8,10],mani:[0,1,2,3,4,6,8,13,14,15],manipul:[5,6],map:8,mapsto:[8,11],marathon:0,march:0,mario:0,mark:[0,1,2,6,12],massot:0,master:0,match:[6,7,8,11],materi:0,math2001:[1,14],math:[0,14],mathbb:[0,1,5,6,7,8,9,10,11,13],mathcal:[9,10],mathemat:[0,1,2,3,4,5,7,10,13,14],mathematician:[0,1,5],mathlib:[0,1],matter:[0,1],matthew:0,matur:0,maxim:4,mayb:[2,9],mb:10,me:[0,2],mean:[1,2,3,4,7,8,9],meant:4,mechan:[2,13],median:0,meg:[8,10],melanchol:8,mem_self:10,member:9,membership:9,memor:3,memori:0,men:9,mental:[0,2,6,9],mention:[1,2,4],mess:[9,10],messag:2,method:[1,2,6,9],microsoft:[0,1],mid:[3,4,5,6,7,9,10],middl:[3,7,11,14,15],midterm:0,might:[0,1,2,3,4,5,6,8,9,10],million:13,mind:0,minim:5,minor:0,minu:0,minut:0,miss:2,misspel:1,mistak:[0,1],mk:10,ml:4,mnemon:1,mod:[3,4,6,8,9,10,11,12,13],mod_cas:[3,4,6,12],mode:0,model:11,modeq:[3,4,6,10],modeq_fac_zero:13,modifi:[2,4,12],modular:[4,6,11,12,14,15],modulo:[3,4,6,10,11,12],monoton:8,moon:8,more:[0,1,2,3,4,5,6,8,9,12,13],morgan:5,morrison:0,most:[0,1,3,4,5,6,7,8,12],mostli:0,motiv:8,motzkin:13,moura:1,mous:3,move:[2,5,12],much:[0,3,4,5,9,13],mul:3,mul_eq_zero:[4,8,9],mul_le_mul_of_nonneg_left:0,multi:2,multicolour:10,multipl:[1,2,4,6,7,9,11,12,13],multipli:1,murril:0,musket:8,must:[1,2,4,5,6,8,9,10],mutual:6,mx:6,my:[0,1,2,4],n1:8,n2:8,n:[0,1,2,3,4,5,6,7,8,9,10,11,12,13],n_1:8,n_2:8,na:6,name:[0,1,2,3,4,5,6,7,8,13],nat:[3,4,6,7,9,10,11,13],natur:[0,1,2,3,4,5,6,7,8,9,10,11,12],navig:1,nc:3,nd:[6,10],ne:[2,4,5,6,7,8,9,11],ne_of_gt:[2,7,8,9],ne_of_lt:[2,5],nearli:[0,7],necessari:[1,7,8],need:[0,1,2,3,4,5,6,7,8,10,11],neg:[1,2,3,6],negat:[1,4,8,9,12,14,15],neither:1,net:1,neutron:8,newli:2,next:[1,2,4,5],nich:6,nine:1,node:10,non:[3,4,6,8],noncomput:8,none:[1,3],nonlinear:0,nonneg:[1,2,4,6],nontrivi:[0,4],nonzero:[2,6],nope:5,nor:1,norm_cast:[6,7],norm_num:[0,13],normal:[8,9,14,15],not_and_or:5,not_dvd_of_exists_lt_and_lt:[3,4,7,9,10,11],not_exist:5,not_foral:[5,11],not_imp:5,not_lt:[5,8],not_lt_of_g:4,not_not:5,not_or:5,not_prim:[4,5],not_prime_on:[4,5],not_superpowered_thre:5,not_superpowered_zero:5,notat:[1,3,4,6,8,9,10],notation:9,note:[1,2,3,4,5,6,7,8,9,10,11,12,14,15],noth:10,notic:[1,2,3,4,5,6,8],notin:9,notion:0,novelti:0,now:[0,1,2,3,4,5,6,7,8,9,10],nudg:0,number:[0,1,2,3,4,5,6,8,9,10,11,12,13,14,15],numer:[1,4,8,12],nx:3,ny:3,object:[0,6,8,9,10],observ:[2,4,5,6,8],obtain:[2,3,4,5,6,7,8,9,10,12],obviou:[1,2,6],obvious:[4,12],occur:[2,3,5,6],odd:[3,4,6,8,9,11],odd_iff_modeq:[4,11],odd_iff_not_even:9,of_a_add_mono:8,off:[0,1,2,3,4,7,9],offer:[0,13],offic:0,often:[0,2,3,9,13],old:7,omen:2,omit:[1,4,6],onc:[1,2,7,8],one:[0,1,2,3,4,5,6,7,8,9,10,11,13],one_prim:5,ones:[2,4],onli:[0,1,2,3,5,6,8,9,10,11,13,14,15],onlin:13,open:[0,1,5,8,10,14],oper:[1,5,8,14,15],operatornam:[0,6,7,8,9,11],opposit:5,option:[1,3,8,9],oral:0,order:[0,1,2,3,5,8],ordin:8,ordinari:4,organ:1,origin:10,other:[0,1,2,4,5,6,7,8,9,10,12],otherwis:[4,5,10],our:[1,2,3,4,5,6,7,8,9],ourselv:2,out:[0,1,2,3,4,5,6,7,8,9,10,12,13,14],outlin:[2,6,13],output:[5,8],outsid:5,outward:5,over:[0,1,3,4,8,10,13,14],overkil:1,overtak:6,own:[0,1,2,5,8,9,10,14],p:[1,2,3,4,5,6,7,8,9,10,11],p_0:6,p_1:6,p_:[6,11],p_comp_i:8,p_m:6,p_n:6,pai:[0,3,4],pain:3,pair:[0,2,5,6,8,10,14],panel:1,paper:[0,1,2,3,6,8,9,10,11],parabola:4,paradox:9,paragraph:[8,9],parenthes:[1,3],pariti:[4,6,11,14,15],part:[0,1,2,4,6,8,12],partial:2,particular:[1,3,4,5,6,7,8],particularli:[0,1,6,8],partli:0,pascal:[11,14,15],pascal_eq:6,pascal_l:6,pascal_symm:6,past:4,patienc:5,patrick:0,pattern:[1,4,6,10],pedant:[1,2,4],peopl:[0,2],per:0,perfectli:2,perform:[0,1,2,4,5,6],perhap:[0,8],period:1,permiss:0,permit:0,phlegmat:8,phrase:[2,4,9],pick:[0,2],pictur:5,piec:[2,6,7],pierr:5,pk:7,pl:7,place:[0,1,3,4,5,6,8],placehold:[1,6],plai:8,plane:10,pleas:[0,14],point:[0,2,3,4,5,6,8,9,11,13],pointer:13,polynomi:1,polyrith:13,pop:1,port:0,portho:8,portion:10,pos_of_dvd_of_po:[3,4],pos_of_mul_pos_left:13,posit:[1,2,3,4,5,6,8,10,12,13],possibl:[0,1,2,3,4,6,9,10,12],pow:[3,6],pow_po:0,pow_thre:3,pow_two:3,power:[1,2,4,5,6,9],pq:[1,5],pr:1,practic:[2,6],practis:5,prec:10,preced:1,precis:[2,6,7,8,9],precondit:2,predic:[4,5,9],predict:2,prefer:0,present:[0,1,5],preserv:1,pretti:[0,1,2,8],previou:[1,2,4,6,8,10],previous:[0,1,2,4,8],primal:[4,13],primari:0,primarili:0,prime:[0,4,5,6,8,11,14,15],prime_test:[4,5],prime_two:[4,5],primit:0,principl:[0,4,5,6],priori:7,priorit:0,probabl:[0,1,2,3,8,10,11],problem1:11,problem2:11,problem3:11,problem4:11,problem4a:11,problem4b:11,problem5:11,problem5a:11,problem5b:11,problem6:11,problem6a:11,problem6b:11,problem:[0,11,13],process:[1,4,5,6],produc:[0,5,6,8,9,12],product:[0,2,4,14,15],program:0,project:[0,13],proof:[0,9,11,12,13,15],prop:[3,4,5,8,9,10,11],proper:[0,7],properti:[2,3,4,5,6,8,9,10],propos:[0,2],proposit:[5,9],prose:[0,2,13],proton:8,prove:[0,2,3,4,5,6,7,8,9,10,11,12,14,15],prover:0,provid:[1,2,3,4,5,6,9,10,11,12],ptruefalsefalsetru:5,punctuat:1,pure:[1,5,9],purpos:[1,4,9],push:[5,12],push_neg:[5,6,8,9,10,11,12],put:[1,2,6,10],putnei:2,py:6,pythagora:[4,7],pythagorean:4,q:[0,1,2,3,4,5,6,7,8,9,11],q_0:6,q_1:6,q_:6,q_n:6,qquad:6,qr:[1,6],quad:[6,9,11],quadrat:2,quantif:4,quantifi:[0,2,4,5,12],quantiti:[1,2,12],question:[1,5],quirk:0,quit:[0,1,2,3,4,6],quotient:[1,6],r:[0,1,2,3,4,5,6,7,8,9,10,11,13],r_0:[6,11],r_1:[6,11],r_:[6,11],r_n:[6,11],rais:[1,5],ramanujan:2,ran:0,rang:[6,8],rare:[2,5],rather:[0,1,2,3,4,6,8,12],ratio:0,ration:[1,2,4,5,7,8,11],re:[2,3,4,5,6,11],reach:[0,6,7,14],read:[0,1,2,7],readabl:13,reader:[0,1,2,13],readi:[0,1],readm:0,real:[0,1,2,4,5,6,8,9,10,11],realiti:2,realli:[0,2,5],rearrang:[1,6,12],reason:[0,1,2,3,4,5,6,7,8,9],recal:[2,3,4,8],recogn:8,recogniz:0,recommend:[1,4,8],record:[2,4,5,6,8,12],recurr:[14,15],recurs:[0,9,11],red:1,redo:2,reduc:[2,4,8,9,10],reduct:13,refer:[0,1,2,5,6,8,9],refl:[3,10],reflect:1,reflex:[14,15],reformul:[4,9],regular:[2,5],rel:[0,1,2,3,4,5,6,8,9,10,11,12,13],relat:[0,1,2,7,9,12,14,15],relev:[1,11],reli:6,relianc:6,remain:[1,4,5],remaind:[1,6],remark:2,rememb:[2,4,5,6],remind:3,renshaw:0,repeat:[2,4,9],repeatedli:[1,3],repetit:8,replac:[12,13],repli:2,repositori:[0,1,14],repres:[2,4,6,10,11],represent:[0,1],request:0,requir:[0,1,2,3,4,5,6,7,8,13],reread:[3,12],research:[0,1],residu:[3,4,12],resolv:[2,9],resourc:0,respect:4,rest:[0,1,2,4],restat:8,result:[0,1,2,4,5,6],revers:[0,1],review:4,rewrit:[1,3,5],rfl:[6,8,10],rh:12,ridden:2,right:[0,1,2,3,4,5,6,7,8,9,10,12],rightarrow:4,rigor:[0,6,10,14],rin:1,ring:[0,1,2,3,4,5,6,7,8,9,10,12,13],rob:0,rock:10,root:[0,4,14,15],rotat:6,rotella:5,rough:8,rule:[0,1,4,5,6,11],run:[1,7,9],rw:[0,1,2,3,4,6,7,8,9,10,11,12,13],ryan:5,s:[0,1,2,4,5,8,9,10,11,13,14,15],s_0:6,s_1:6,s_:6,s_m:6,s_n:6,sai:[0,2,6,8,10],said:[2,5,8],sake:[2,4,9,12],same:[0,1,2,3,4,5,6,7,8,10],sampl:6,sanguin:8,saniti:[5,6],satisfi:[2,4,6,8],saw:[2,4],school:[0,1,2,4,6],scissor:10,scope:13,scott:0,scratch:[1,5,6,11,13],screen:1,screenshar:0,search:13,searchabl:13,second:[0,1,2,4,5,6,8,9,11],secondli:[4,8],section:[0,1,2,3,4,5,6,7,8,9,10,11,12],see:[0,1,2,3,5,6,8,9,10,11],seek:8,seem:[1,2,5],seen:[1,2,3,6,8],select:12,self:[6,8],semest:0,send:[3,8],sens:[2,5,6],sensit:1,sentenc:[1,2,3,8,9],separ:[1,2,4,5,6],sequenc:[1,2,5,6,8,9,11,13],seriou:8,serv:2,session:0,set:[0,1,2,4,5,6,7,8,10,13,14,15],settl:5,setup:[2,4,6,9],seven:4,sever:[0,1,3,6,8],shape:0,share:0,shave:9,shortcut:[3,14,15],shorten:[1,2],shorter:[4,5],shorthand:[1,2,4,5,6,10],should:[0,1,2,3,5,8,9],show:[1,2,3,4,5,6,7,8,9,10,11],side:[1,2,4,12],sight:3,sign:[0,1],signal:4,signific:0,silent:[1,2,6],silli:5,sim:10,similar:[1,2,3,4,5,6,8],similarli:[1,2,4,8],simpl:[1,6],simple_induct:[6,9,13],simpler:[1,2,4,5,8],simpli:[1,2,9],simplifi:[1,2,3,5,8,9],simultan:[1,2],sin:1,sinc:[0,1,2,3,4,5,6,7,8,9,10,13],singl:[0,1,2,3,6,9],situat:[1,2,4,5,7,9],size:[1,4,6,8,9],sizeatleastthre:9,sizeatleasttwo:9,sketch:10,skill:0,skip:4,slick:1,slight:4,slightli:[5,9],slow:0,small:[0,1,6,13],smaller:[1,2,6],smallest:[2,4],so:[0,1,2,3,4,5,6,7,8,9,10,11,12],solut:[0,11],solv:[0,1,2,3,4,5,6,8,9,11,12,13],some:[0,1,2,3,4,5,6,7,9,10,13],someon:2,someth:[0,1,2,3,8,9],sometim:[1,2,4,5,6,9],somewhat:6,somewher:[1,2],sorri:[1,2,3,4,5,6,8,9,10,11],sought:7,sound:[4,10],sourc:[0,13],space:1,speak:1,special:[2,4,6,7,8,9],specif:[3,5,8,12],specifi:[4,6,9,12],spent:0,sphinx:0,split:[1,2,6,8,11,12],split_if:6,spot:3,spring:0,sq_le_sq:4,sq_ne_two:[2,7],squar:[0,1,2,4,11,14,15],st:1,staff:0,stage:[0,2],stand:[1,2,6,8,9],standard:[0,1,2,3,9],star:[2,4,6,7,8,10],start:[0,1,2,3,4,6,7,8,9,11,13],state:[0,1,2,3,4,5,6,8,9,11,13],statement:[0,1,2,3,4,5,6,7,8,9,12,13],statu:1,steadili:0,step:[0,1,3,5,7,11,13,14,15],still:[1,2,3,5,12],stop:3,straight:1,straightforward:2,streamlin:[0,9],strict:9,strictli:[0,2,3,4,6,8,9,11],strong:[0,7,11,14,15],structur:[0,5,6,14,15],struggl:0,student:[0,1,2,5],studi:[1,2,4,5,6,8,9],studio:1,style:[0,1,2,3,5,6,7,11,13],sub:[2,3,9,12,13],subatom:8,subject:[0,2],submit:[0,11],subsequ:[0,6],subset:[9,10],subset_def:9,subseteq:[9,10],substitut:[0,1,2,12,13],subtler:8,subtleti:[1,2],subtract:[1,2,8,13],subtractioncommmonoid:13,succeed:2,success:[1,6],successfulli:6,suffic:[0,2,4,5,8,9,10],suffici:[0,2,4,6,8,11],suggest:[2,5,6,11],suit:1,sum:[2,6,11],summari:0,sun:8,superpow:5,superpowered_on:5,support:0,suppos:[1,2,3,4,5,6,7,8,9,10,11],sure:1,surfac:13,surject:[9,10,11,14,15],surjective_of_intertwin:8,surpris:[0,2,6],surround:1,suspect:0,suspici:6,sustain:0,sweat:6,symbol:[0,1,2,3,4,5,9],symm:[3,10],symmetr:[11,14,15],symmetri:[3,10],synonym:2,syntax:[0,2,6,8],system:[0,1,2,8,11],t:[0,1,2,3,4,5,6,7,8,9,11],t_0:6,t_1:6,t_:6,t_eq:6,t_n:6,ta:0,tabl:[0,5,6,11],tactic:[0,1,2,3,4,5,6,7,8,9,11,14,15],tag:[6,7],take:[0,1,2,3,4,5,8,12,13],taken:[0,3,5],task:[2,6],taught:[0,1],tauto:[8,9,10],taxi:2,teach:0,team:1,technic:0,techniqu:[0,1,4,6,7,11],tell:[2,13],templat:11,tempt:1,term:[0,1,3,4,6,8,9,12],termin:6,termination_bi:[6,7,11],terminolog:3,test:[3,4,7],text:[0,1,2,3,6,8,9,11],textbook:[0,1],than:[0,1,2,3,4,6,7,8,10,11,12,13],thank:0,thei:[0,1,2,3,4,5,6,8,9,10,13],them:[0,1,2,3,4,5,6,7,8,12],themselv:[1,9,10],theorem:[0,2,3,5,11],theoret:0,theori:[0,9,14,15],therefor:[1,2,4,5,6,7,8,10],thi:[1,2,3,4,5,6,7,8,9,10,11,12,14,15],thing:[1,3,4,6],think:[1,3,5,6,7,8,11],third:[1,8],thoma:0,those:[4,5,6,7,8,9],though:[2,3,5,9],thousand:[0,1],three:[1,4,7,9],through:[0,1,2,6,9,13],throwawai:3,thu:[2,3,4,6,7,8,11],time:[0,1,2,3,4,5,6,8,10,11],tin:0,tip:[14,15],tire:6,tl:4,togeth:[1,2,3,4,5,6,10,13],ton:9,too:[1,2,4,5,6,8,9],took:5,tool:[0,2,3,4,7],toolbox:0,toolkit:3,top:[1,2],topic:0,topolog:13,total:0,toward:[0,1],town:9,track:[0,2,6],trade:1,tradit:[0,5,6],train:0,tran:[3,10],transform:[1,2,4,5],transit:[0,1,3,11,14,15],translat:[0,2,3,4],treat:4,treatment:0,triangl:[4,11,14,15],tribalanc:5,trick:[2,7,8,14,15],tripl:4,trivial:6,truetruefalsefalsetruefalsetruefalsefalsetruetruefalsetruetruefalsefalsefalsetruefalsetru:5,truetruetruefalsetruefalsetruefalsefalsefalsefalsetru:5,truetruetruefalsetruetruetruefalsefalsefalsefalsetru:5,truetruetruefalsetruetruetruefalsetruefalsefalsefals:5,truth:[0,5],truth_tabl:5,turn:[2,6,7,9,10],tweak:2,twelv:2,twice:0,twisti:9,two:[0,1,2,3,4,5,8,9,10,11,12,14,15],two_step_induct:[6,13],two_step_induction_from_starting_point:[6,13],twostepinduct:13,type:[0,1,3,6,10,14,15],typeset:0,typic:[0,1,2,3,6,12,13],u:[1,8,9],u_0:9,u_:9,u_n:9,ub:1,unambigu:0,unconvent:1,under:[0,1,2,3,4,5,6,8],underli:[4,9,10],underlin:[1,6],understand:[1,2,4,5,6],unfamiliar:[5,6],unfavor:2,unfold:[3,6,8,9,12],unforgiv:0,unfortun:3,union:9,uniqu:[6,8,14,15],univ:9,univers:[0,4,5,9,12,14],unlik:6,unnecessari:1,unseen:0,until:[0,2,3],unusu:[0,1],up:[0,1,2,3,4,5,6,7,8,9,10],updat:[0,2,3],upgrad:6,upper:[1,4,6,12],upper_bound_fmod1:6,upper_bound_fmod2:6,us:[0,1,2,3,4,5,6,7,8,9,10,11,12],useless:0,usual:[0,1,2,3,5,6,8,9],uv:1,uy:1,v:[1,8,9],vacuou:6,valid:[1,2,5,6,7,12],valu:[2,4,8],vari:1,variabl:[1,2,3,4,5,8,10,12],variant:[3,6,8],variou:[0,5],vb:1,ve:[1,2,3,4,5],vein:5,veri:[0,1,2,3,4,5,6,7],verifi:[1,2],vernacular:0,versa:[7,9,12],version:[2,3,4,6,7,8,9,10,11,12,13],vertic:2,via:6,vice:[7,9,12],view:[0,2,5],visibl:2,visual:[0,1,2,3,6,10],vocabulari:0,vphantom:1,vs:1,vscode:3,vx:1,w:1,wa:[0,1,2,3,4,5,6,7,8,9],wai:[0,1,2,3,4,5,6,8,9,10],walk:2,want:[1,2,3,4,5,6,8,13],warmup:5,warn:[1,3],wast:8,water:8,we:[0,1,2,3,4,5,6,7,8,9,10,13],weaken:13,websit:13,week:0,well:[0,1,2,4,6,7,8,11,13],were:[0,1,2,3,4,5,7,8,9],what:[0,1,2,3,4,6,7,8],when:[0,1,2,3,4,5,6,7,8,9,10,12],whenev:6,where:[1,2,3,5,6,8],wherea:1,whether:[1,3,4,5,6,8,9,12,13],whew:3,which:[0,1,2,3,4,5,6,7,8,9,10,11,12,13],white:8,who:[0,1,5,9],whole:[1,9],whose:[1,2,3,4,7,8,9,11,12],why:[0,1,2,4,5,6,8],wikimedia:6,wild:[1,2],window:[2,3],winter:0,wish:[2,3,6,8,13],wit:[0,2,9,12],within:[2,3,6],without:[0,1,2,3,5,6,9],won:[0,3],wonder:[1,3,4,5],word:[0,1,2,3,4,5,9,11],work:[0,1,2,3,4,5,6,7,8,9,11,12,13],world:[0,1],worri:5,wors:5,worth:5,worthi:0,would:[0,1,2,4,5,6,7,8,9,13],wrap:13,wrapper:[9,13],write:[0,1,2,3,4,5,6,7,8,9,11,13,14],writer:1,written:[0,1,2,3,4,5,6,7,8,9,14],wrong:[1,5],wrote:[1,8],x0:8,x1:[8,9,10],x2:[8,9,10],x3:9,x:[1,2,3,4,5,6,7,8,9,10,11,12],x_0:[6,8],x_1:[8,9,10],x_1x_2:8,x_2:[8,9,10],x_3:9,x_:6,x_k:6,x_n:6,xa:[6,7],xt:2,xy:[2,3,4,6],xz:7,y1:[8,10],y2:[8,10],y:[1,2,3,4,5,6,7,8,9,10,11,12],y_0:[6,11],y_1:[8,10],y_2:[8,10],y_:[6,11],y_n:[6,11],yb:[6,7],yd:7,year:[0,1],yet:[0,1,2,3,5,6,7],you:[0,1,2,3,4,5,6,8,9,10,11,12,13],your:[0,1,2,3,4,5,6,11,12,13,14],yourself:[2,3,5,6,8],yt:3,yx:1,z:[0,1,2,3,5,7,8,9,10,11],zero:[0,2,7],zifi:8,zmod:[3,4,6,8,9,10,11],zoo:9},titles:["Introduction","1. Proofs by calculation","2. Proofs with structure","3. Parity and divisibility","4. Proofs with structure, II","5. Logic","6. Induction","7. Number theory","8. Functions","9. Sets","10. Relations","Homework","Index of Lean tactics","Transitioning to mainstream Lean","The mechanics of proof","header for testing"],titleterms:{"0":11,"1":11,"2":11,"3":11,"4":11,"5":11,"6":11,"7":11,"8":11,"b\u00e9zout":[3,6],"case":2,"function":[6,8],A:1,And:2,For:4,If:4,Or:2,The:[5,6,7,9,14],There:4,about:0,acknowledg:0,addit:3,advanc:13,algorithm:[4,6,13],all:4,analogu:13,antisymmetr:10,arithmet:3,biject:8,book:[0,13],calcul:[1,3],composit:8,contradict:4,contradictori:4,corollari:[6,7],cube:3,defin:6,definit:[3,4,5,6,8,9,10],divis:[3,4,6],equal:1,equival:[5,10],euclid:7,euclidean:6,exampl:[1,2,3,4,5,6,8,9,10],exclud:5,exercis:[1,2,3,4,5,6,8,9,10],exist:[2,4],form:5,gauss:7,header:15,homework:11,hypothes:4,ident:[3,6],ii:4,implic:4,index:12,induct:6,inequ:1,infinit:7,inject:8,instructor:0,intermedi:2,introduct:[0,6,9],invok:2,law:5,lean:[0,1,12,13],lemma:[2,3,4,5,7],logic:5,mainstream:13,mani:7,mathlib:13,mechan:14,middl:5,modular:3,multipl:3,negat:[3,5],normal:5,note:0,number:7,onli:4,oper:9,origin:13,pariti:3,pascal:6,power:3,prime:7,problem:[1,2,3,4,5,6,8,9,10],product:8,proof:[1,2,3,4,5,6,7,8,10,14],proposit:[6,8],prove:1,recurr:6,recurs:6,reflex:[3,10],relat:[6,10],root:7,rule:3,s:[3,6,7],set:9,shortcut:1,solut:[1,2,3,4,5,6,8,9,10],squar:[3,7],step:[2,6],strong:6,structur:[2,4],subtract:3,surject:8,symmetr:10,tactic:[12,13],test:15,theorem:[4,6,7,8,10],theori:[3,7],thi:[0,13],tip:1,transit:[10,13],triangl:6,trick:1,two:[6,7],type:[8,9],uniqu:4,us:13,valu:6}})
\ No newline at end of file
+Search.setIndex({docnames:["00_Introduction","01_Proofs_by_Calculation","02_Proofs_with_Structure","03_Parity_and_Divisibility","04_Proofs_with_Structure_II","05_Logic","06_Induction","07_Number_Theory","08_Functions","09_Sets","10_Relations","Homework","Index_of_Tactics","Mainstream_Lean","index","latexindex"],envversion:{"sphinx.domains.c":2,"sphinx.domains.changeset":1,"sphinx.domains.citation":1,"sphinx.domains.cpp":4,"sphinx.domains.index":1,"sphinx.domains.javascript":2,"sphinx.domains.math":2,"sphinx.domains.python":3,"sphinx.domains.rst":2,"sphinx.domains.std":2,sphinx:56},filenames:["00_Introduction.rst","01_Proofs_by_Calculation.rst","02_Proofs_with_Structure.rst","03_Parity_and_Divisibility.rst","04_Proofs_with_Structure_II.rst","05_Logic.rst","06_Induction.rst","07_Number_Theory.rst","08_Functions.rst","09_Sets.rst","10_Relations.rst","Homework.rst","Index_of_Tactics.rst","Mainstream_Lean.rst","index.rst","latexindex.rst"],objects:{},objnames:{},objtypes:{},terms:{"0":[1,2,3,4,5,6,7,8,9,10,14],"01_proofs_by_calcul":1,"02_proving_equalities_in_lean":1,"03_tips_and_trick":1,"1":[0,1,2,3,4,5,6,7,8,9,10,12,14],"10":[0,1,2,3,4,6,8,9,10,11],"100":[6,11],"10000":6,"1024":6,"104":3,"1048576":6,"1096":6,"10b":1,"10n":[4,8],"10t":1,"11":[1,2,3,4,6,9,11],"11n":3,"12":[2,3,4,8,12],"126":6,"12n":2,"13":[0,3,4,12],"14":[1,4],"15":[3,4,6],"16":[3,4,6,9],"16384":6,"1650":5,"17":[1,2,5,6],"1729":2,"1732":5,"18":[2,3,4,6],"19":4,"19349":6,"1960":1,"19684":5,"1cm":1,"2":[0,1,2,3,4,5,6,7,8,9,10,12,14],"20":[0,1,4,6,9],"2001":[0,1,14],"2013":0,"2014":1,"2022":0,"2023":0,"21":6,"2207":6,"23":11,"24":[3,4,6],"25":[0,2,12],"252":6,"256":6,"257":5,"26":[3,4],"267":6,"27":4,"28":5,"2a":[1,2,3,4,8],"2a_0":6,"2a_1":6,"2a_2":6,"2a_k":6,"2a_n":6,"2ab":1,"2an":1,"2anbm":1,"2b":[1,2,3,4,7,8],"2c":[1,8],"2f":8,"2k":[3,4,6,7,9],"2l":9,"2m":[1,6,8],"2n":[1,2,3,6,8,11],"2q":1,"2q_":6,"2r":2,"2r_":[6,11],"2s":[1,7,11],"2s_":6,"2t":3,"2t_":6,"2v":1,"2x":[1,2,3,4,6,8,11],"2x_1":8,"2x_2":8,"2x_k":6,"2x_n":6,"2xy":12,"2y":[1,2,3,8,9],"3":[0,1,2,3,4,5,6,7,8,9,10,12,14],"30":[4,5,11],"300":7,"31":6,"316837008400094222150776738483768236006420971486980607":6,"32":6,"33":11,"33m":11,"34":3,"35":6,"36":2,"38":11,"38n":11,"39":4,"3a":[2,3,4,8,10],"3ab":[1,2],"3b":[3,4],"3c":[1,10],"3c_n":6,"3d_":6,"3k":4,"3m":[2,3],"3n":[1,3,6,11],"3p":3,"3r":3,"3s":11,"3s_n":6,"3t":[1,2],"3u":1,"3w":1,"3x":[2,8,9,11],"3y":[1,3,4,8],"3z":8,"4":[0,1,2,3,4,5,6,7,8,9,10,12,14],"40":[3,4,9],"4096":6,"42":9,"4294967297":5,"45":4,"450":7,"46":2,"4623":6,"47":6,"49":2,"4a":[1,3,9,11],"4ab":1,"4anbm":1,"4b":[1,4],"4c_n":6,"4k":[6,9],"4m":2,"4n":[2,4,9],"4q":[1,11],"4u":1,"4x":[1,4],"4y":3,"5":[0,1,2,3,4,5,6,7,8,9,10,12,14],"50":[3,10],"55":0,"56":6,"59":6,"5a":[1,3,4,9],"5b":[1,2,4],"5b_":[6,11],"5d_k":6,"5d_n":6,"5k":[9,11],"5m":8,"5m_1":8,"5m_2":8,"5n":[1,3,4,9,11],"5q":4,"5s":3,"5t":[2,9],"5x":[1,3,8],"6":[0,1,2,3,4,5,6,7,8,9,14],"628":1,"63":[3,4],"64":6,"641":5,"65":3,"65537":5,"66":11,"6700417":5,"69":2,"6a":[1,3],"6b_n":[6,11],"6k":9,"6n":6,"6p_":6,"7":[0,1,2,3,4,5,6,7,8,9,10,14],"70":6,"72":1,"75":0,"79":[4,11],"7b":1,"7n":[3,9],"7t":1,"8":[0,1,2,3,4,5,6,7,8,9,14],"80":0,"84":2,"85":2,"88":3,"8a":[1,3,4,9],"8b":[1,3],"8n":8,"8n_1":8,"8n_2":8,"8x":[1,11],"9":[0,1,2,3,4,6,8,9,10,11],"97":[4,11],"9k":9,"\u03b1":[2,5,9,10,11],"\u03b2":[5,10],"\u03b3":10,"\u1d9c":9,"\u2115":[2,3,4,5,6,7,8,9,10,11],"\u211a":[1,2,4,6,8,9,11],"\u211d":[1,2,4,5,6,8,9,10,11],"\u2124":[1,2,3,4,5,6,7,8,9,10,11],"abstract":[5,8,10,13],"b\u00e9zout":[7,14,15],"break":[0,2,4,7,8],"case":[0,1,3,4,5,6,7,8,9,10,11,12,14,15],"class":[0,3,4,5,10],"default":3,"do":[0,1,2,3,4,5,6,7,8,11,13],"final":[0,1,2,4,5,7,8,12],"function":[0,3,9,10,11,14,15],"gr\u00f6bner":13,"hq\u2081":4,"hq\u2082":4,"import":[1,2,3,4,5,6,10],"int":[3,4,6,9,10,11,13],"long":[1,2,4,5,6],"mul_left_cancel\u2080":13,"new":[0,1,2,3,4,6,8,9,12],"return":[5,10],"short":[0,1,6],"switch":6,"throw":[0,3],"true":[0,2,3,4,5,6,8,9,10,11,12],"try":[1,2,3,5,6,8,10],"while":[1,5,12],A:[0,2,3,4,5,6,7,8,9,10,12,13,14,15],And:[1,3,5,6,8,9,14,15],As:[1,2,3,4,5,6,8],At:[0,1,2,4,5,6,8,9],Be:1,But:[0,1,2,3,4,5,6,7,8,9],By:[2,4,5,6,7,8,9,10],For:[0,1,2,3,5,6,7,8,9,10,14,15],If:[0,1,2,3,5,6,7,8,9,10,11,12,13,14,15],In:[0,1,2,3,4,5,6,7,8,9,10,13],Is:5,It:[0,1,2,3,4,5,6,7,9,10,11],No:2,On:[1,2,3,9],One:[1,2,4],Or:[3,7,14,15],Such:[3,8],That:[1,2,3,4,5,6,7,9],The:[0,1,2,3,4,8,10,11,13,15],Then:[1,2,3,4,5,6,7,8,9,10],There:[0,1,2,3,5,6,7,8,9,14,15],These:[0,2,4,5,6,7,8,13,14],To:[1,2,4,5,6,7,8,9,13],With:[6,12],_:[1,2,3,4,5,6,7,8,9,10,11],_x:8,_y:8,a1:[8,10],a2:[8,10],a_0:6,a_1:[6,10],a_2:[6,10],a_3:6,a_4:6,a_5:6,a_:[6,8],a_k:6,a_m:6,a_mono:8,a_n:[6,8],ab:[1,2,3,5,7,11],abl:[1,3,12],about:[1,2,3,4,5,6,7,8,9,14,15],abov:[1,2,3,4,5,6,7,8,9],abs_le_of_sq_le_sq:[2,4],absolut:6,abus:0,ac:3,accept:1,access:2,accord:[3,4,6,8,9,12],accordingli:4,account:1,acknowledg:[14,15],acronym:6,act:2,actual:[0,1,2,3,4,7],ad:[1,2,6,10,13],adapt:[1,2,5,6,8,9],add:[0,1,2,3],addarith:[1,2,4,6,7,8,9,12,13],addit:[1,2,5,8,12],adjust:13,adopt:0,advanc:[1,6],advantag:1,aesop:13,af:[1,10],after:[0,1,2,3,4,5,6,8,9,10,12,13],afterward:2,again:[1,2,3,6,7,9],agre:[5,6],aim:14,air:8,ak:[3,10],aka:0,algebra:[0,1,2,6,12,13],algorithm:[0,11,14,15],all:[0,1,2,3,5,6,7,8,9,10,11,13,14,15],allow:[1,2,4,5],almost:[0,1,6],alon:[1,6],along:[2,6,10],aloud:0,alpha:10,alreadi:[0,1,2,3,4,5],also:[0,1,2,3,4,5,6,7,8,9,10,11],altern:[0,2,3,8,9,12],although:[2,3,5,6],alwai:[5,6,7,13],am:[1,10],ambigu:7,ami:10,amount:[0,6,9],an:[0,1,2,3,4,5,6,7,8,9,10,11,12,13],analogu:6,analysi:[0,8],analyz:4,ancient:[5,7],angl:4,ani:[0,2,3,4,5,6,8,10,11,13],annot:[0,1,4],announc:2,anoth:[1,2,3,4,5,6,7,8,9,10,13],answer:9,anteced:[4,12],antisymmetr:[14,15],antisymmetri:2,anyth:[4,5],anywai:2,anywher:1,apart:[2,12],appar:6,appear:[0,1,2,3,4,11],appendic:14,appendix:[0,13],appli:[1,2,3,4,5,6,7,8,9,10,11,12],applic:[2,6],appris:0,approach:[1,6,8,9,11],appropri:1,approxim:4,ar:[0,1,2,3,4,5,6,7,8,9,10,11,12,13,14],arami:8,arbitrari:[4,8],arg:10,argument:[0,1,2,4,6,7],aris:8,arithmet:[4,6,11,12,14,15],around:[1,9],arrow:7,ask:[1,2,4,6,12],assess:0,assign:0,assist:[0,1],associ:[1,13,14],assum:[1,2,4,8,12],assumpt:[5,8,9],atho:8,atom:0,attempt:[6,12],attent:0,attribut:6,author:14,auto:0,autograd:11,autom:[0,8],automat:[0,1,5,6],av:1,avail:[0,2,3,4,6,7,12],avigad:0,avoid:[0,1,6,7,13],awai:5,awar:13,awkward:5,ax:[3,6,11],axiom:[5,8],b1:8,b2:8,b:[1,2,3,4,5,6,7,8,9,10,11,13],b_0:[6,11],b_1:[6,11],b_2:6,b_3:6,b_:[6,11],b_k:6,b_n:[6,11],ba:1,back:[0,1,2,3,5,7],background:0,backward:[0,6],banana:2,barber:9,base:[0,6,7,13],basic:[0,5,6,13],bc:[1,7],bd:3,becaus:[0,2,4,5,6,8,13],becom:[0,2,6,8,12],been:[0,1,2,4,5,6,8,14],befor:[1,2,3,4,5,6,8],begin:[1,2,4,5,6,7],beginn:1,behaviour:[2,10],behind:9,being:[0,1,2,3,6,9,10],believ:6,belong:9,below:[2,4,6,8,9,11],ben:2,bernoulli:6,best:13,beta:10,beth:10,better:[3,4,6,7,8,9,13],better_prime_test:[4,5,11],between:[0,2,3,4,5,6,7,11],beyond:[0,8,13],bezout:[6,7],bi:[4,10],big:[0,1,2],biject:[10,14,15],bijective_iff_exists_invers:[8,10],bijective_of_invers:8,bilingu:0,bit:[4,5,6],bk:4,bl:10,blackboard:[0,4],block:[0,1,2,6,13],blue:1,bm:1,bn:[1,10],board:13,book:[1,2,3,4,5,6,7,8,9,12,14,15],both:[0,1,2,3,4,5,6,8,9,12],bottom:[1,2],bound:[1,4,6,12],bq:[3,4,6,11],brahmagupta:[1,7],branch:9,breakdown:0,breather:3,brief:0,bring:3,broader:8,broken:2,brought:[2,5],brown:5,build:[0,1,9],built:[2,3,4,6],bundl:6,bv:1,by_cas:[5,6,8,9,11,12],byd:7,c:[1,2,3,4,6,7,8,9,10,11,13],c_0:6,c_1:6,c_:6,c_n:6,ca:1,cab:2,calc:[1,2,3,4,5,6,7,8,9,10,11],calcul:[0,2,5,6,7,13,14,15],calculu:0,call:[0,1,2,4,5,6,7,9],came:1,can:[0,1,2,3,4,5,6,7,8,9,10,11,13],cancel:[0,1,2,3,4,6,7,8,10,11,12,13],candid:8,cannot:[1,4,7],canon:[0,6],cap:9,capabl:[6,8,13],capston:7,care:[0,14],carefulli:[1,4,12],carneiro:0,carri:[0,1,2,7,9,13],cast:[1,7],casual:2,caus:[1,2],caveat:5,cb:[1,10],cdot:[1,2,3,4,5,6,7,8,9,10,11,12],ce:1,celesti:8,central:[5,7],certain:[0,2,9,13],certainli:[1,5],cf:[1,10],chain:1,chanc:3,chang:[0,2,6],chapter:[0,1,2,3,4,5,6,7,8,9,10],character:[4,6],characteris:4,check:[1,2,3,4,5,6,8,9,11,12,13],check_equality_of_explicit_set:9,checkabl:8,choic:[0,4,8],choler:8,choos:[1,2,8],chosen:2,circ:8,circl:7,circul:0,circular:6,claim:[4,7],classic:[0,1,2],classroom:0,claus:6,clean:9,clear:[2,6],clearer:4,clearli:[0,4,5,8],clever:[1,2,7],click:3,cliqu:10,close:[1,4,6,7,8],closer:2,cloud:[0,1,14],co:8,code:[0,1,2,3,13,14],codespac:0,codomain:8,coeffici:1,collect:[9,13],colloqui:4,colon:1,colour:10,com:[1,14],combin:[0,1,3,4,5,6,8,9,10,13],come:[0,1,2,3,8],comfort:0,command:[3,5,8],comment:14,commentari:0,common:[1,2,4,6,7,8,12],commonli:[0,1,2],commun:[0,13],comp:[8,10],compact:3,compar:[2,4,5,6,8,9,11,12],comparison:[1,12],complain:1,complement:9,complet:[0,2,6],complex:[2,5,8],complic:[0,1,2,4,6,8],compon:8,compos:5,composit:[14,15],comprehens:[0,5],comput:[0,1,5,6,14],concept:[0,2,3,4,5,9],conceptu:[5,8],concern:3,concis:1,conclud:[0,1,2,4,6,7,8,12],conclus:[1,2,4,7],concret:[5,6],condit:2,confirm:[2,8,9],confus:3,congruenc:[3,4,6,12],congruent:[3,4,6,10,11],connect:[0,1,2,4,10],consecut:[3,4,7],consequ:2,consid:[1,2,3,4,5,6,7,8,9,10,11],consider:2,consist:[1,2,7,8,10],consolid:3,constant:[1,6,13],constitu:2,constitut:[0,7,8],constrain:0,construct:[6,8],constructor:[2,3,4,5,6,7,8,9,10,12],consult:[1,12],contain:[0,1,2,4,7,8,9,13],context:[3,8,9],continu:[0,2,6],contradict:[5,6,7,8,9,12,14,15],contradictori:[8,12,14,15],contraposit:5,contribut:5,conv:[5,9],conveni:[3,4,5,6,8,9,10],convent:[0,2,6],convers:[0,4,8,9,10],convert:[4,5,7,8,11,12],copi:2,core:0,corollari:8,correct:[0,1,3,9,14],correctli:9,correspond:[0,1,2,3,7],could:[1,3,4,7,8],counteract:1,coupl:4,cours:[0,4,5,13,14],courteou:1,cover:[0,1,2,3,5,13],creat:[1,2,4,8],creativ:2,credit:[6,11],crucial:3,ctrl:3,cube:2,cup:9,current:[0,2,3,6],cursor:2,curv:0,custom:0,cx:8,d:[1,2,3,6,7,10],d_0:6,d_1:6,d_4:6,d_5:6,d_:6,d_k:6,d_n:6,dagger:7,dai:0,danger:6,date:7,david:0,davidson:2,dbe:1,de:[1,5],deal:[0,1,2,3,14],dealt:8,debt:4,decidableeq:[8,10],decim:6,decreas:[6,7],deduc:[1,2,4,5,6,11],deduct:[0,1,2,4,12],deeper:5,def:[3,4,5,6,8,9,10,11],defin:[0,4,7,8,9,10,11],definit:[0,2,11,12,14,15],degre:1,delai:5,delet:[2,3,12],deliber:13,delic:[1,6],demonstr:5,denot:[2,3,6,7,8,9,10],depart:0,depend:[1,3,4,5,6,11],deriv:[4,8,10],describ:[6,8,9],descript:9,design:[0,1,9],desir:[2,4,5,6,9],detail:[0,2,3,6,13],determin:[1,2,10],develop:[0,1,6,7],devot:0,dialect:[0,13],did:[2,4,5,8],differ:[0,1,2,3,4,6,7,8,9,10,12,13],difficult:[2,7,8],difficulti:1,direct:[1,4,5,6,8,10],direction:10,directli:[1,2,3,4,6,9,11],discov:[1,13],discoveri:[5,13],discret:6,discuss:[1,2,3,4,8,9,13],disequ:2,disguis:9,displai:[2,3,6,7,8,9],disprov:[8,9,11],distinct:2,distinguish:0,div:6,divid:[1,3,6,11],divis:[0,1,2,5,7,8,11,13,14,15],divisor:[3,6,7,8],dk:7,dl:7,document:13,doe:[0,3,4,5,6,8,9,11,13],doesn:[1,4,5,8],domain:8,don:[0,1,2,3,4,5,6,8,9,11],done:[1,2,3,4,5,6,7,8,10,13],dot:3,doubl:[1,3],down:[1,2,6,7,8,9],download:[1,14],draw:[1,2,7,10],dream:0,drop:[0,1],dry:10,dsimp:[3,4,5,6,7,8,9,10,11,12],due:6,dull:2,durat:3,dvd:3,dvd_factori:[6,7],dvd_iff_modeq:4,dx:6,dy:6,dz:7,e:[1,3,8,10],each:[0,1,2,4,5,6,8,9,10,12],earli:[0,2,8,14],earlier:[2,4,5],earth:8,easi:[0,1,2,3,6,13],easier:[0,2,4],easili:[0,1,4],eb:10,ebner:0,ed:10,edmond:5,effect:[2,3,8,12],effici:[0,4,8,13],effort:0,either:[1,2,3,4,5,6,7,8,9,11],electron:8,eleg:6,element:[7,8,9,10],elementari:[0,3,6],elimin:[1,13],els:[2,6,10],elsewher:[0,1,8],email:0,emphasi:6,empti:9,emptyset:9,enclos:6,encount:[0,3,4,5,6],end:[1,2,5,6,13],endgam:6,endless:0,enforc:0,english:[0,2],enjoi:[0,13],enough:[0,2,3,6,8],ensu:8,ensur:0,enthusiasm:0,enthusiast:0,environ:[0,1],eq_of_rel:10,eq_or_lt_of_l:[4,6],eq_zero_or_eq_zero_of_mul_eq_zero:[2,4,11],eq_zero_or_po:10,equal:[0,2,4,5,6,7,8,9,12,14,15],equat:[1,2,4,5,8],equiv:[3,4,6,8,9,10,11],equival:[0,7,8,9,11,12,14,15],equivalenceclass:10,erron:1,error:[0,1,6],especi:0,establish:[0,1,2,4,6,7],etc:[1,2,4,6,7,11,12,13],euclid:[0,14,15],euclid_lemma:7,euclid_lemma_pow:7,euclidean:[11,14,15],euler:5,eval:[6,8],evalu:6,even:[0,1,3,4,5,6,7,8,9,11],even_iff_modeq:4,even_iff_not_odd:[4,9],even_of_pow_even:[6,7],even_or_odd:[3,4,6,11],eventu:6,everi:[1,2,3,4,5,6,8,9,10],everyth:[0,7,8,9,11],everywher:3,exact:[6,13],exactli:[1,2,3,4,6],exam:7,examin:0,exampl:[0,7,11,13],except:[2,11],exclud:[11,14,15],exercis:[0,7,11],exhaust:8,exist:[0,3,5,6,7,8,9,10,11,12,13,14,15],existenti:[0,2,3,12],exists_factor_of_not_prim:[5,6],exists_inverse_of_biject:8,exists_prime_factor:[6,7],existsunique_modeq_lt:[4,6],exot:6,expand:[1,8,12],expect:[0,2,8,13],experi:[0,1,6],experienc:0,experiment:0,expert:[0,5,8],explain:[0,1,2,6,9],explan:6,explicit:[1,6,8],explicitli:[0,1,2,4,7,9],exploit:1,explor:[7,13],expon:6,exponenti:12,express:[0,1,2,3,4,6,9],ext:[8,9,10],extend:[6,11],extens:1,extension:[8,9],extra:[0,1,2,3,4,6,7,8,9,12,13],extract_pow_two:6,extrem:[7,13],ey:1,f1:10,f2:10,f:[1,6,8,9,10,11],f_0:6,f_1:6,f_1f_0:6,f_:6,f_bound:6,f_k:6,f_m:6,f_n:6,facil:6,fact:[0,1,2,3,4,5,6,7,8,10,12],factor:[2,3,4,5,6,7,12],factori:[6,7],factorial_po:[6,7],fail:[1,2,5],fairli:[0,5,6,8],fall:0,fals:[0,4,5,8,9,10,11,12],falsehood:5,famili:[5,6],familiar:[0,1,2,9],famou:[5,6,7],far:[1,2,6,7,8,12],fdiv:6,featur:[0,1,2,3,4,6,9,13],feedback:[0,1],feel:[1,2,3,4],fermat:5,few:[0,1,6,13],fewer:[0,6],fibonacci:[6,8],fiddli:7,field_simp:6,fifti:0,figur:2,file:[0,1],fill:[0,1,2,4,6,8,11],find:[0,2,3,4,5,6,7,8,11,13],fine:[1,7,8],finger:3,finish:[2,4,8],finit:[4,6,8,9,10],fire:8,first:[0,1,2,3,4,5,6,7,8,9,10,11,12,13],firstli:[4,8],five:[1,9],fix:[5,6],fixm:8,flatter:0,flexibl:[0,1,6,8],fluenci:0,fmod:6,fmod_add_fdiv:6,fmod_lt_of_po:6,fmod_nonneg_of_po:6,focu:[0,1],follow:[1,2,3,4,5,6,7,8,9,10,11,12],foo:2,footnot:[0,1,2,3,4,5,6,8,9],foral:[4,5,9,11,12],forall_sufficiently_larg:[4,6,11],fordham:[0,2,14],foreign:0,forev:6,form:[1,2,4,6,7,8,10,12,14,15],formal:[0,1,3,4,5,13,14],former:[4,9],formul:9,formula:[4,5,6,8],forth:0,fortun:8,forum:12,forward:0,found:[0,6,7,11],foundat:9,founded:[0,6,7],four:[1,8],four_not_prim:5,four_prim:5,fourier:13,fourth:1,frac:[1,2,3,4,5,6,8,11],frankli:8,free:[0,4,8,11],frequent:[3,6],from:[0,1,2,3,4,5,6,7,8,9,11,12,13],front:1,full:[1,2,3,5,6,8,9,13],fulli:[0,2],fun:[7,8,10,11,13],fundament:[4,7],further:[1,2,8,13],furthermor:1,fussi:0,futur:[0,2,4,5,6,8],g1:8,g2:8,g:[2,8,10],g_1:8,g_2:8,gabriel:0,game:5,gauss:[14,15],gauss_lemma:7,gcd:[6,7,11],gcd_dvd:6,gcd_dvd_left:[6,7],gcd_dvd_right:[6,7],gcd_maxim:6,gcd_nonneg:[6,7],gcongr:13,ge:[1,2,4,6,9,11],gener:[1,2,3,4,5,6,7,8,9,13],geq:[1,2,3,4,5,6,7,9,11],get:[0,1,2,4,6,8,11,12],github:[0,1,14],gitpod:[0,1,14],give:[1,2,3,4,5,6,7,8],given:[1,2,3,4,6,7,8,9,10,12],go:[0,1,2,3,8],goal:[0,1,2,3,4,5,6,8,9,12],goe:[5,6,9],good:[0,5,8],googl:12,grade:0,grader:0,gradescop:[0,11],gradual:2,grammar:[4,5],grant:[0,3],graph:10,great:3,greater:[1,2,4,6,7,11],greatest:[6,7,8],greedili:1,greek:[0,5,7],grew:0,group:0,guarante:7,guardrail:0,guess:[3,10,13],h0:8,h1:[1,2,3,4,5,6,7,8,9,10,11],h1m:4,h2:[1,2,3,4,5,6,7,8,9,10,11],h3:[1,2,4,5,6,9],h4:[1,2,4,6],h5:[1,4],h6:[1,9],h7:1,h8:1,h9:1,h:[1,2,3,4,5,6,7,8,9,10,11],h_div:4,h_gauss:7,h_gt:7,h_inj:8,h_le:7,h_moon:8,h_pyth:4,h_refl:10,h_sun:8,h_surj:8,h_symm:10,h_tran:10,ha1:4,ha1b:10,ha2:4,ha2b:10,ha:[0,1,2,3,4,5,6,7,8,9,10,11,13],hab:[2,3,4,6,7,8,10,11],hack:0,had:[0,1,2,4,9],half:[4,5],halfwai:[0,1],hammack:[2,3,6],hand:[1,2,4,5,6,8,10,12,13],handl:[7,8,13],handwritten:4,hap1:7,hap2:7,happen:[1,2,4,5,6],hard:[0,2,3,6,8,11],harder:[2,4],hardi:2,hardli:5,hasn:5,hat:8,haunt:0,have:[0,1,2,3,4,5,6,7,8,9,10,11,12,13,14],haven:[2,7],hb1:4,hb2:4,hb:[2,3,4,6,7,8],hbc:[3,10,11],hbk:7,hc:[2,4],hd:[6,7],he:2,head:[1,3,5,14],heartfelt:0,heather:14,heavi:0,help:[1,2,6,12,13],henc:[6,7,8],henceforth:8,here:[0,1,2,3,4,5,6,7,8,9],herself:2,hertz:0,hf1a:10,hf1b:10,hf2a:10,hf2b:10,hf:[8,9,10],hfact:4,hfg1:10,hfg2:10,hfg:8,hfx:9,hg:8,hgcd:7,hgcd_1:7,hgcd_p:7,hgf:8,hi:[2,8],high:[0,1,2,4],him:2,himself:9,hk1:[4,5,6],hk:[3,4,5,6,7,8,9,10],hkl:4,hkp:[4,5],hl1:4,hl2:4,hl:[4,6,7,9,10],hm1:[4,8],hm2:[4,8],hm:[2,3,4,6,8],hm_left:4,hm_right:4,hmn:6,hmp:4,hmp_le:4,hmt:4,hn0:[2,7],hn1:4,hn2:[4,6,7],hn:[1,2,3,4,5,6,8,9,11],hneg:4,hold:[5,7,9,10],homework:[0,4,7,14],honest:0,honestli:1,hood:4,hope:[0,2],hopefulli:4,horizon:8,horizont:1,hour:0,hover:3,how:[0,1,2,3,4,5,6,8,9,13,14],howev:[6,8],hp1:7,hp2:[5,7],hp:[2,3,4,5,6,7],hpn:7,hpo:4,hpq:[3,5],hq:[3,5],hqr:3,hr1:4,hr2:4,hr3:4,hr:[3,4,6],hrmacbeth:[1,14],hs:[3,6,9],hspace:1,hst:9,ht:[1,2,7,9,11],htp:4,http:[1,14],human:[1,2,6],humour:8,hundr:0,hx1:[8,9],hx1x2:8,hx2:[8,9],hx:[1,2,3,4,5,6,8,9,10,11],hxt:2,hxx1:8,hxx2:8,hxy:10,hy:[1,2,3,4,6,8,10],hyperlink:13,hypothes:[0,1,2,3,6,7,8,12,13,14,15],hypothesi:[1,2,3,4,6,7,8,12],hyz:10,hz:7,i:[0,1,2,3,4,5,6,8,9,11,13],id:[1,8,10],idea:[1,4,5,6,7,8,9,11],ident:[1,7,8,14,15],identifi:2,idiomat:0,ignor:1,ih1:6,ih2:6,ih:[6,7,8],ih_left:6,ih_right:6,ii:[0,2,9,14,15],ill:2,imag:6,imagin:5,immedi:[1,2,4,6,8],imo:1,implement:0,impli:[1,2,4,10],implic:[12,14,15],implicitli:[0,1,4,6],importantli:1,imposs:[0,4,7],improv:6,incant:9,includ:[0,2,4,8,9,10,11,13],incorrect:1,increasingli:[0,6],inde:[2,3,4,5,6,7,8,9,10],independ:[2,13],index:[6,8,14,15],indian:1,indic:[1,2,6,9,11,12],individu:[0,1],induct:[0,7,8,10,11,13,14,15],induction_from_starting_point:[6,7,8,13],inequ:[0,2,4,5,6,12,13,14,15],infer:[1,9],infinit:[4,14,15],infinitud:0,infix:10,inform:[0,1,4,5,9],infoview:[1,2,6,7,8,9],infrastructur:0,ingredi:2,initi:[1,2,3],inject:[9,10,11,14,15],input:[6,7,8],insert:4,insid:[0,1,3,5],inspect:[2,8,12],instal:[0,1],instant:[0,1],instanti:6,instead:[0,1,2,4,5,7,8,11],instruct:[0,1],instructor:[12,14,15],integ:[0,1,2,3,4,6,7,8,9,10,11,12],intellectu:0,interact:[0,1,2,7,13],interest:[0,1,2,3,6],intermedi:[1,3,5,14,15],intern:13,internet:12,interpret:1,intersect:9,intertwin:8,interval_cas:[4,6,9,12],interview:0,intrepid:0,intro:[0,4,5,6,7,8,9,10,12],introduc:[0,1,2,3,4,5,6,7,8,9,10,12],introduct:[4,14,15],intuit:[5,8],invers:[8,10],invis:2,invoc:8,invok:[0,1,3,4,6,7,8,9,12,13,14,15],involv:[1,2,4,5,6,8],inward:[5,12],irrat:[5,7],irrat_aux:7,irrat_aux_wf:7,irration:0,isn:1,issu:[6,13],iter:[0,9],its:[1,2,3,4,5,6,7,8,9,10,12,13],itself:[2,6,8,9],j:4,jack:8,jeremi:0,jo:10,joint:6,jointli:6,joseph:5,just:[0,1,2,3,4,5,6,7,8,9,10,11],justif:[0,1,2,4,6,7],justifi:[1,2,6],juxtapos:0,k:[3,4,5,6,7,8,9,10,11],k_contra:7,keep:[0,2,6],kei:[1,2,7],kept:0,keyboard:3,keyword:[1,2],kind:[1,3,4,5,6,7,8,13],kl:[4,10],knock:9,know:[0,1,5,6,7,10],knowledg:[0,2],known:[0,1,2,4,5,6,7],kq:6,ky:6,l01:0,l:[3,4,5,6,7,8,9,10],l_mul_add_r_mul:6,label:4,land:[2,4,5,9,11,12],languag:[0,2,9,10,14],larg:[4,6,11],larger:[2,4,6],last:[1,2,3,5,6,8,9],later:[0,1,2,3,4,6,7],latter:[4,9],law:[2,11,14,15],ldot:[1,2,4,6],le:[1,2,3,4,5,6,7,8,9,10,11],le_add_of_nonneg_right:13,le_antisymm:[2,4,6,8,10,11],le_induct:13,le_of_dvd:[3,4,10],le_of_pow_le_pow:0,le_or_gt:2,le_or_lt:[4,7,8,9],le_or_succ_l:[2,4,5,11],lead:6,lean:[2,3,4,5,6,7,8,9,11,14,15],learn:[0,1,2,3,4,5,6],least:[2,3,4,9],leav:[1,2,4,5,8],lectur:[0,2,4,7,12,14],led:1,left:[0,1,2,4,5,6,7,8,9,10,12],leftarrow:4,leftrightarrow:[4,5],lemma:[0,6,8,11,12,13,14,15],leonardo:1,leonhard:5,leq:[1,2,4,10],less:[2,3,4,10],let:[0,1,2,3,4,5,6,7,8,9,10,11],level:[0,6,8,10,13,14],lewi:0,lh:12,li:[3,4,7,11],liber:9,librari:[0,1,2,3,4,5,13],life:2,lift:7,lightli:0,like:[0,1,2,3,4,5,6,7,8,9,12],likewis:[1,4,5,6,10],limit:[0,6],linarith:13,line:[1,2,3,4,5,6,8,9,10,11,12,13],linear:13,link:0,list:[2,4,6,9],literatur:13,littl:[2,6,10],live:[0,1,2],ll:[1,2,3,5,8],lnot:[4,5,11,12],local:10,logic:[0,2,3,4,6,7,8,9,11,12,13,14,15],longer:[0,2],look:[0,1,2,3,4,5,6,9,12],lor:[2,3,4,5,9,11,12],lose:0,lot:[3,8],low:6,lower:[6,12],lower_bound_fmod1:6,lower_bound_fmod2:6,lt:2,lt_add_of_pos_right:13,lt_fmod_of_neg:6,lt_of_le_of_n:6,lt_of_pow_lt_pow:13,lt_or_l:4,lt_trichotomi:8,luck:13,lx:7,ly:2,m1:8,m2:8,m:[1,2,3,4,5,6,8,9,10,11],m_1:8,m_2:8,mac:3,macbeth:14,macro:9,made:10,magic:1,mai:[0,1,2,3,4,6,8,9,13],main:[0,2,3,6,7,11],mainstream:[0,14,15],major:[0,3,13],make:[0,1,2,3,4,5,6,7,8,10],mani:[0,1,2,3,4,6,8,13,14,15],manipul:[5,6],map:8,mapsto:[8,11],marathon:0,march:0,mario:0,mark:[0,1,2,6,12],massot:0,master:0,match:[6,7,8,11],materi:0,math2001:[1,14],math:[0,14],mathbb:[0,1,5,6,7,8,9,10,11,13],mathcal:[9,10],mathemat:[0,1,2,3,4,5,7,10,13,14],mathematician:[0,1,5],mathlib:[0,1],matter:[0,1],matthew:0,matur:0,maxim:4,mayb:[2,9],mb:10,me:[0,2],mean:[1,2,3,4,7,8,9],meant:4,mechan:[2,13],median:0,meg:[8,10],melanchol:8,mem_self:10,member:9,membership:9,memor:3,memori:0,men:9,mental:[0,2,6,9],mention:[1,2,4],mess:[9,10],messag:2,method:[1,2,6,9],microsoft:[0,1],mid:[3,4,5,6,7,9,10],middl:[3,7,11,14,15],midterm:0,might:[0,1,2,3,4,5,6,8,9,10],million:13,mind:0,minim:5,minor:0,minu:0,minut:0,miss:2,misspel:1,mistak:[0,1],mk:10,ml:4,mnemon:1,mod:[3,4,6,8,9,10,11,12,13],mod_cas:[3,4,6,12],mode:0,model:11,modeq:[3,4,6,10],modeq_fac_zero:13,modifi:[2,4,12],modular:[4,6,11,12,14,15],modulo:[3,4,6,10,11,12],monoton:8,moon:8,more:[0,1,2,3,4,5,6,8,9,12,13],morgan:5,morrison:0,most:[0,1,3,4,5,6,7,8,12],mostli:0,motiv:8,motzkin:13,moura:1,mous:3,move:[2,5,12],much:[0,3,4,5,9,13],mul:3,mul_eq_zero:[4,8,9],mul_le_mul_of_nonneg_left:0,multi:2,multicolour:10,multipl:[1,2,4,6,7,9,11,12,13],multipli:1,murril:0,musket:8,must:[1,2,4,5,6,8,9,10],mutual:6,mx:6,my:[0,1,2,4],n1:8,n2:8,n:[0,1,2,3,4,5,6,7,8,9,10,11,12,13],n_1:8,n_2:8,na:6,name:[0,1,2,3,4,5,6,7,8,13],nat:[3,4,6,7,9,10,11,13],natur:[0,1,2,3,4,5,6,7,8,9,10,11,12],navig:1,nc:3,nd:[6,10],ne:[2,4,5,6,7,8,9,11],ne_of_gt:[2,7,8,9],ne_of_lt:[2,5],nearli:[0,7],necessari:[1,7,8],need:[0,1,2,3,4,5,6,7,8,10,11],neg:[1,2,3,6],negat:[1,4,8,9,12,14,15],neither:1,net:1,neutron:8,newli:2,next:[1,2,4,5],nich:6,nine:1,node:10,non:[3,4,6,8],noncomput:8,none:[1,3],nonlinear:0,nonneg:[1,2,4,6],nontrivi:[0,4],nonzero:[2,6],nope:5,nor:1,norm_cast:[6,7],norm_num:[0,13],normal:[8,9,14,15],not_and_or:5,not_dvd_of_exists_lt_and_lt:[3,4,7,9,10,11],not_exist:5,not_foral:[5,11],not_imp:5,not_lt:[5,8],not_lt_of_g:4,not_not:5,not_or:5,not_prim:[4,5],not_prime_on:[4,5],not_superpowered_thre:5,not_superpowered_zero:5,notat:[1,3,4,6,8,9,10],notation:9,note:[1,2,3,4,5,6,7,8,9,10,11,12,14,15],noth:10,notic:[1,2,3,4,5,6,8],notin:9,notion:0,novelti:0,now:[0,1,2,3,4,5,6,7,8,9,10],nudg:0,number:[0,1,2,3,4,5,6,8,9,10,11,12,13,14,15],numer:[1,4,8,12],nx:3,ny:3,object:[0,6,8,9,10],observ:[2,4,5,6,8],obtain:[2,3,4,5,6,7,8,9,10,12],obviou:[1,2,6],obvious:[4,12],occur:[2,3,5,6],odd:[3,4,6,8,9,11],odd_iff_modeq:[4,11],odd_iff_not_even:9,of_a_add_mono:8,off:[0,1,2,3,4,7,9],offer:[0,13],offic:0,often:[0,2,3,9,13],old:7,omen:2,omit:[1,4,6],onc:[1,2,7,8],one:[0,1,2,3,4,5,6,7,8,9,10,11,13],one_prim:5,ones:[2,4],onli:[0,1,2,3,5,6,8,9,10,11,13,14,15],onlin:13,open:[0,1,5,8,10,14],oper:[1,5,8,14,15],operatornam:[0,6,7,8,9,11],opposit:5,option:[1,3,8,9],oral:0,order:[0,1,2,3,5,8],ordin:8,ordinari:4,organ:1,origin:10,other:[0,1,2,4,5,6,7,8,9,10,12],otherwis:[4,5,10],our:[1,2,3,4,5,6,7,8,9],ourselv:2,out:[0,1,2,3,4,5,6,7,8,9,10,12,13,14],outlin:[2,6,13],output:[5,8],outsid:5,outward:5,over:[0,1,3,4,8,10,13,14],overkil:1,overtak:6,own:[0,1,2,5,8,9,10,14],p:[1,2,3,4,5,6,7,8,9,10,11],p_0:6,p_1:6,p_:[6,11],p_comp_i:8,p_m:6,p_n:6,pai:[0,3,4],pain:3,pair:[0,2,5,6,8,10,14],panel:1,paper:[0,1,2,3,6,8,9,10,11],parabola:4,paradox:9,paragraph:[8,9],parenthes:[1,3],pariti:[4,6,11,14,15],part:[0,1,2,4,6,8,12],partial:2,particular:[1,3,4,5,6,7,8],particularli:[0,1,6,8],partli:0,pascal:[11,14,15],pascal_eq:6,pascal_l:6,pascal_symm:6,past:4,patienc:5,patrick:0,pattern:[1,4,6,10],pedant:[1,2,4],peopl:[0,2],per:0,perfectli:2,perform:[0,1,2,4,5,6],perhap:[0,8],period:1,permiss:0,permit:0,phlegmat:8,phrase:[2,4,9],pick:[0,2],pictur:5,piec:[2,6,7],pierr:5,pk:7,pl:7,place:[0,1,3,4,5,6,8],placehold:[1,6],plai:8,plane:10,pleas:[0,14],point:[0,2,3,4,5,6,8,9,11,13],pointer:13,polynomi:1,polyrith:13,pop:1,port:0,portho:8,portion:10,pos_of_dvd_of_po:[3,4],pos_of_mul_pos_left:13,posit:[1,2,3,4,5,6,8,10,12,13],possibl:[0,1,2,3,4,6,9,10,12],pow:[3,6],pow_po:0,pow_thre:3,pow_two:3,power:[1,2,4,5,6,9],pq:[1,5],pr:1,practic:[2,6],practis:5,prec:10,preced:1,precis:[2,6,7,8,9],precondit:2,predic:[4,5,9],predict:2,prefer:0,present:[0,1,5],preserv:1,pretti:[0,1,2,8],previou:[1,2,4,6,8,10],previous:[0,1,2,4,8],primal:[4,13],primari:0,primarili:0,prime:[0,4,5,6,8,11,14,15],prime_test:[4,5],prime_two:[4,5],primit:0,principl:[0,4,5,6],priori:7,priorit:0,probabl:[0,1,2,3,8,10,11],problem1:11,problem2:11,problem3:11,problem4:11,problem4a:11,problem4b:11,problem5:11,problem5a:11,problem5b:11,problem6:11,problem6a:11,problem6b:11,problem:[0,11,13],process:[1,4,5,6],produc:[0,5,6,8,9,12],product:[0,2,4,14,15],program:0,project:[0,13],proof:[0,9,11,12,13,15],prop:[3,4,5,8,9,10,11],proper:[0,7],properti:[2,3,4,5,6,8,9,10],propos:[0,2],proposit:[5,9],prose:[0,2,13],proton:8,prove:[0,2,3,4,5,6,7,8,9,10,11,12,14,15],prover:0,provid:[1,2,3,4,5,6,9,10,11,12],ptruefalsefalsetru:5,punctuat:1,pure:[1,5,9],purpos:[1,4,9],push:[5,12],push_neg:[5,6,8,9,10,11,12],put:[1,2,6,10],putnei:2,py:6,pythagora:[4,7],pythagorean:4,q:[0,1,2,3,4,5,6,7,8,9,11],q_0:6,q_1:6,q_:6,q_n:6,qquad:6,qr:[1,6],quad:[6,9,11],quadrat:2,quantif:4,quantifi:[0,2,4,5,12],quantiti:[1,2,12],question:[1,5],quirk:0,quit:[0,1,2,3,4,6],quotient:[1,6],r:[0,1,2,3,4,5,6,7,8,9,10,11,13],r_0:[6,11],r_1:[6,11],r_:[6,11],r_n:[6,11],rais:[1,5],ramanujan:2,ran:0,rang:[6,8],rare:[2,5],rather:[0,1,2,3,4,6,8,12],ratio:0,ration:[1,2,4,5,7,8,11],re:[2,3,4,5,6,11],reach:[0,6,7,14],read:[0,1,2,7],readabl:13,reader:[0,1,2,13],readi:[0,1],readm:0,real:[0,1,2,4,5,6,8,9,10,11],realiti:2,realli:[0,2,5],rearrang:[1,6,12],reason:[0,1,2,3,4,5,6,7,8,9],recal:[2,3,4,8],recogn:8,recogniz:0,recommend:[1,4,8],record:[2,4,5,6,8,12],recurr:[14,15],recurs:[0,9,11],red:1,redo:2,reduc:[2,4,8,9,10],reduct:13,refer:[0,1,2,5,6,8,9],refl:[3,10],reflect:1,reflex:[14,15],reformul:[4,9],regular:[2,5],rel:[0,1,2,3,4,5,6,8,9,10,11,12,13],relat:[0,1,2,7,9,12,14,15],relev:[1,11],reli:6,relianc:6,remain:[1,4,5],remaind:[1,6],remark:2,rememb:[2,4,5,6],remind:3,renshaw:0,repeat:[2,4,9],repeatedli:[1,3],repetit:8,replac:[12,13],repli:2,repositori:[0,1,14],repres:[2,4,6,10,11],represent:[0,1],request:0,requir:[0,1,2,3,4,5,6,7,8,13],reread:[3,12],research:[0,1],residu:[3,4,12],resolv:[2,9],resourc:0,respect:4,rest:[0,1,2,4],restat:8,result:[0,1,2,4,5,6],revers:[0,1],review:4,rewrit:[1,3,5],rfl:[6,8,10],rh:12,ridden:2,right:[0,1,2,3,4,5,6,7,8,9,10,12],rightarrow:4,rigor:[0,6,10,14],rin:1,ring:[0,1,2,3,4,5,6,7,8,9,10,12,13],rob:0,rock:10,root:[0,4,14,15],rotat:6,rotella:5,rough:8,rule:[0,1,4,5,6,11],run:[1,7,9],rw:[0,1,2,3,4,6,7,8,9,10,11,12,13],ryan:5,s:[0,1,2,4,5,8,9,10,11,13,14,15],s_0:6,s_1:6,s_:6,s_m:6,s_n:6,sai:[0,2,6,8,10],said:[2,5,8],sake:[2,4,9,12],same:[0,1,2,3,4,5,6,7,8,10],sampl:6,sanguin:8,saniti:[5,6],satisfi:[2,4,6,8],saw:[2,4],school:[0,1,2,4,6],scissor:10,scope:13,scott:0,scratch:[1,5,6,11,13],screen:1,screenshar:0,search:13,searchabl:13,second:[0,1,2,4,5,6,8,9,11],secondli:[4,8],section:[0,1,2,3,4,5,6,7,8,9,10,11,12],see:[0,1,2,3,5,6,8,9,10,11],seek:8,seem:[1,2,5],seen:[1,2,3,6,8],select:12,self:[6,8],semest:0,send:[3,8],sens:[2,5,6],sensit:1,sentenc:[1,2,3,8,9],separ:[1,2,4,5,6],sequenc:[1,2,5,6,8,9,11,13],seriou:8,serv:2,session:0,set:[0,1,2,4,5,6,7,8,10,13,14,15],settl:5,setup:[2,4,6,9],seven:4,sever:[0,1,3,6,8],shape:0,share:0,shave:9,shortcut:[3,14,15],shorten:[1,2],shorter:[4,5],shorthand:[1,2,4,5,6,10],should:[0,1,2,3,5,8,9],show:[1,2,3,4,5,6,7,8,9,10,11],side:[1,2,4,12],sight:3,sign:[0,1],signal:4,signific:0,silent:[1,2,6],silli:5,sim:10,similar:[1,2,3,4,5,6,8],similarli:[1,2,4,8],simpl:[1,6],simple_induct:[6,9,13],simpler:[1,2,4,5,8],simpli:[1,2,9],simplifi:[1,2,3,5,8,9],simultan:[1,2],sin:1,sinc:[0,1,2,3,4,5,6,7,8,9,10,13],singl:[0,1,2,3,6,9],situat:[1,2,4,5,7,9],size:[1,4,6,8,9],sizeatleastthre:9,sizeatleasttwo:9,sketch:10,skill:0,skip:4,slick:1,slight:4,slightli:[5,9],slow:0,small:[0,1,6,13],smaller:[1,2,6],smallest:[2,4],so:[0,1,2,3,4,5,6,7,8,9,10,11,12],solut:[0,11],solv:[0,1,2,3,4,5,6,8,9,11,12,13],some:[0,1,2,3,4,5,6,7,9,10,13],someon:2,someth:[0,1,2,3,8,9],sometim:[1,2,4,5,6,9],somewhat:6,somewher:[1,2],sorri:[1,2,3,4,5,6,8,9,10,11],sought:7,sound:[4,10],sourc:[0,13],space:1,speak:1,special:[2,4,6,7,8,9],specif:[3,5,8,12],specifi:[4,6,9,12],spent:0,sphinx:0,split:[1,2,6,8,11,12],split_if:6,spot:3,spring:0,sq_le_sq:4,sq_ne_two:[2,7],squar:[0,1,2,4,11,14,15],st:1,staff:0,stage:[0,2],stand:[1,2,6,8,9],standard:[0,1,2,3,9],star:[2,4,6,7,8,10],start:[0,1,2,3,4,6,7,8,9,11,13],state:[0,1,2,3,4,5,6,8,9,11,13],statement:[0,1,2,3,4,5,6,7,8,9,12,13],statu:1,steadili:0,step:[0,1,3,5,7,11,13,14,15],still:[1,2,3,5,12],stop:3,straight:1,straightforward:2,streamlin:[0,9],strict:9,strictli:[0,2,3,4,6,8,9,11],strong:[0,7,11,14,15],structur:[0,5,6,14,15],struggl:0,student:[0,1,2,5],studi:[1,2,4,5,6,8,9],studio:1,style:[0,1,2,3,5,6,7,11,13],sub:[2,3,9,12,13],subatom:8,subject:[0,2],submit:[0,11],subsequ:[0,6],subset:[9,10],subset_def:9,subseteq:[9,10],substitut:[0,1,2,12,13],subtler:8,subtleti:[1,2],subtract:[1,2,8,13],subtractioncommmonoid:13,succeed:2,success:[1,6],successfulli:6,suffic:[0,2,4,5,8,9,10],suffici:[0,2,4,6,8,11],suggest:[2,5,6,11],suit:1,sum:[2,6,11],summari:0,sun:8,superpow:5,superpowered_on:5,support:0,suppos:[1,2,3,4,5,6,7,8,9,10,11],sure:1,surfac:13,surject:[9,10,11,14,15],surjective_of_intertwin:8,surpris:[0,2,6],surround:1,suspect:0,suspici:6,sustain:0,sweat:6,symbol:[0,1,2,3,4,5,9],symm:[3,10],symmetr:[11,14,15],symmetri:[3,10],synonym:2,syntax:[0,2,6,8],system:[0,1,2,8,11],t:[0,1,2,3,4,5,6,7,8,9,11],t_0:6,t_1:6,t_:6,t_eq:6,t_n:6,ta:0,tabl:[0,5,6,11],tactic:[0,1,2,3,4,5,6,7,8,9,11,14,15],tag:[6,7],take:[0,1,2,3,4,5,8,12,13],taken:[0,3,5],task:[2,6],taught:[0,1],tauto:[8,9,10],taxi:2,teach:0,team:1,technic:0,techniqu:[0,1,4,6,7,11],tell:[2,13],templat:11,tempt:1,term:[0,1,3,4,6,8,9,12],termin:6,termination_bi:[6,7,11],terminolog:3,test:[3,4,7],text:[0,1,2,3,6,8,9,11],textbook:[0,1],than:[0,1,2,3,4,6,7,8,10,11,12,13],thank:0,thei:[0,1,2,3,4,5,6,8,9,10,13],them:[0,1,2,3,4,5,6,7,8,12],themselv:[1,9,10],theorem:[0,2,3,5,11],theoret:0,theori:[0,9,14,15],therefor:[1,2,4,5,6,7,8,10],thi:[1,2,3,4,5,6,7,8,9,10,11,12,14,15],thing:[1,3,4,6],think:[1,3,5,6,7,8,11],third:[1,8],thoma:0,those:[4,5,6,7,8,9],though:[2,3,5,9],thousand:[0,1],three:[1,4,7,9],through:[0,1,2,6,9,13],throwawai:3,thu:[2,3,4,6,7,8,11],time:[0,1,2,3,4,5,6,8,10,11],tin:0,tip:[14,15],tire:6,tl:4,togeth:[1,2,3,4,5,6,10,13],ton:9,too:[1,2,4,5,6,8,9],took:5,tool:[0,2,3,4,7],toolbox:0,toolkit:3,top:[1,2],topic:0,topolog:13,total:0,toward:[0,1],town:9,track:[0,2,6],trade:1,tradit:[0,5,6],train:0,tran:[3,10],transform:[1,2,4,5],transit:[0,1,3,11,14,15],translat:[0,2,3,4],treat:4,treatment:0,triangl:[4,11,14,15],tribalanc:5,trick:[2,7,8,14,15],tripl:4,trivial:6,truetruefalsefalsetruefalsetruefalsefalsetruetruefalsetruetruefalsefalsefalsetruefalsetru:5,truetruetruefalsetruefalsetruefalsefalsefalsefalsetru:5,truetruetruefalsetruetruetruefalsefalsefalsefalsetru:5,truetruetruefalsetruetruetruefalsetruefalsefalsefals:5,truth:[0,5],truth_tabl:5,turn:[2,6,7,9,10],tweak:2,twelv:2,twice:0,twisti:9,two:[0,1,2,3,4,5,8,9,10,11,12,14,15],two_step_induct:[6,13],two_step_induction_from_starting_point:[6,13],twostepinduct:13,type:[0,1,3,6,10,14,15],typeset:0,typic:[0,1,2,3,6,12,13],u:[1,8,9],u_0:9,u_:9,u_n:9,ub:1,unambigu:0,unconvent:1,under:[0,1,2,3,4,5,6,8],underli:[4,9,10],underlin:[1,6],understand:[1,2,4,5,6],unfamiliar:[5,6],unfavor:2,unfold:[3,6,8,9,12],unforgiv:0,unfortun:3,union:9,uniqu:[6,8,14,15],univ:9,univers:[0,4,5,9,12,14],unlik:6,unnecessari:1,unseen:0,until:[0,2,3],unusu:[0,1],up:[0,1,2,3,4,5,6,7,8,9,10],updat:[0,2,3],upgrad:6,upper:[1,4,6,12],upper_bound_fmod1:6,upper_bound_fmod2:6,us:[0,1,2,3,4,5,6,7,8,9,10,11,12],useless:0,usual:[0,1,2,3,5,6,8,9],uv:1,uy:1,v:[1,8,9],vacuou:6,valid:[1,2,5,6,7,12],valu:[2,4,8],vari:1,variabl:[1,2,3,4,5,8,10,12],variant:[3,6,8],variou:[0,5],vb:1,ve:[1,2,3,4,5],vein:5,veri:[0,1,2,3,4,5,6,7],verifi:[1,2],vernacular:0,versa:[7,9,12],version:[2,3,4,6,7,8,9,10,11,12,13],vertic:2,via:6,vice:[7,9,12],view:[0,2,5],visibl:2,visual:[0,1,2,3,6,10],vocabulari:0,vphantom:1,vs:1,vscode:3,vx:1,w:1,wa:[0,1,2,3,4,5,6,7,8,9],wai:[0,1,2,3,4,5,6,8,9,10],walk:2,want:[1,2,3,4,5,6,8,13],warmup:5,warn:[1,3],wast:8,water:8,we:[0,1,2,3,4,5,6,7,8,9,10,13],weaken:13,websit:13,week:0,well:[0,1,2,4,6,7,8,11,13],were:[0,1,2,3,4,5,7,8,9],what:[0,1,2,3,4,6,7,8],when:[0,1,2,3,4,5,6,7,8,9,10,12],whenev:6,where:[1,2,3,5,6,8],wherea:1,whether:[1,3,4,5,6,8,9,12,13],whew:3,which:[0,1,2,3,4,5,6,7,8,9,10,11,12,13],white:8,who:[0,1,5,9],whole:[1,9],whose:[1,2,3,4,7,8,9,11,12],why:[0,1,2,4,5,6,8],wikimedia:6,wild:[1,2],window:[2,3],winter:0,wish:[2,3,6,8,13],wit:[0,2,9,12],within:[2,3,6],without:[0,1,2,3,5,6,9],won:[0,3],wonder:[1,3,4,5],word:[0,1,2,3,4,5,9,11],work:[0,1,2,3,4,5,6,7,8,9,11,12,13],world:[0,1],worri:5,wors:5,worth:5,worthi:0,would:[0,1,2,4,5,6,7,8,9,13],wrap:13,wrapper:[9,13],write:[0,1,2,3,4,5,6,7,8,9,11,13,14],writer:1,written:[0,1,2,3,4,5,6,7,8,9,14],wrong:[1,5],wrote:[1,8],x0:8,x1:[8,9,10],x2:[8,9,10],x3:9,x:[1,2,3,4,5,6,7,8,9,10,11,12],x_0:[6,8],x_1:[8,9,10],x_1x_2:8,x_2:[8,9,10],x_3:9,x_:6,x_k:6,x_n:6,xa:[6,7],xt:2,xy:[2,3,4,6],xz:7,y1:[8,10],y2:[8,10],y:[1,2,3,4,5,6,7,8,9,10,11,12],y_0:[6,11],y_1:[8,10],y_2:[8,10],y_:[6,11],y_n:[6,11],yb:[6,7],yd:7,year:[0,1],yet:[0,1,2,3,5,6,7],you:[0,1,2,3,4,5,6,8,9,10,11,12,13],your:[0,1,2,3,4,5,6,11,12,13,14],yourself:[2,3,5,6,8],yt:3,yx:1,z:[0,1,2,3,5,7,8,9,10,11],zero:[0,2,7],zifi:8,zmod:[3,4,6,8,9,10,11],zoo:9},titles:["Introduction","1. Proofs by calculation","2. Proofs with structure","3. Parity and divisibility","4. Proofs with structure, II","5. Logic","6. Induction","7. Number theory","8. Functions","9. Sets","10. Relations","Homework","Index of Lean tactics","Transitioning to mainstream Lean","The mechanics of proof","header for testing"],titleterms:{"0":11,"1":11,"2":11,"3":11,"4":11,"5":11,"6":11,"7":11,"8":11,"b\u00e9zout":[3,6],"case":2,"function":[6,8],A:1,And:2,For:4,If:4,Or:2,The:[5,6,7,9,14],There:4,about:0,acknowledg:0,addit:3,advanc:13,algorithm:[4,6,13],all:4,analogu:13,antisymmetr:10,arithmet:3,biject:8,book:[0,13],calcul:[1,3],composit:8,contradict:4,contradictori:4,corollari:[6,7],cube:3,defin:6,definit:[3,4,5,6,8,9,10],divis:[3,4,6],equal:1,equival:[5,10],euclid:7,euclidean:6,exampl:[1,2,3,4,5,6,8,9,10],exclud:5,exercis:[1,2,3,4,5,6,8,9,10],exist:[2,4],form:5,gauss:7,header:15,homework:11,hypothes:4,ident:[3,6],ii:4,implic:4,index:12,induct:6,inequ:1,infinit:7,inject:8,instructor:0,intermedi:2,introduct:[0,6,9],invok:2,law:5,lean:[0,1,12,13],lemma:[2,3,4,5,7],logic:5,mainstream:13,mani:7,mathlib:13,mechan:14,middl:5,modular:3,multipl:3,negat:[3,5],normal:5,note:0,number:7,onli:4,oper:9,origin:13,pariti:3,pascal:6,power:3,prime:7,problem:[1,2,3,4,5,6,8,9,10],product:8,proof:[1,2,3,4,5,6,7,8,10,14],proposit:[6,8],prove:1,recurr:6,recurs:6,reflex:[3,10],relat:[6,10],root:7,rule:3,s:[3,6,7],set:9,shortcut:1,solut:[1,2,3,4,5,6,8,9,10],squar:[3,7],step:[2,6],strong:6,structur:[2,4],subtract:3,surject:8,symmetr:10,tactic:[12,13],test:15,theorem:[4,6,7,8,10],theori:[3,7],thi:[0,13],tip:1,transit:[10,13],triangl:6,trick:1,two:[6,7],type:[8,9],uniqu:4,us:13,valu:6}})
\ No newline at end of file