Skip to content

Commit

Permalink
Merge pull request #37 from int-y1/fix-typo
Browse files Browse the repository at this point in the history
Fix typos
  • Loading branch information
jmadiot authored Mar 7, 2024
2 parents 36117f6 + 1e1635f commit e8bad9f
Show file tree
Hide file tree
Showing 3 changed files with 6 additions and 6 deletions.
6 changes: 3 additions & 3 deletions index.html
Original file line number Diff line number Diff line change
Expand Up @@ -374,7 +374,7 @@ <h3 id='17' class='formalized'><a href='http://www.cs.ru.nl/~freek/100/#17'>17.
</ul>
<p class='existing'>Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower</p></div>

<h3 id='18' class='formalized'><a href='http://www.cs.ru.nl/~freek/100/#18'>18. Liouville’s Theorem and the Construction of Trancendental Numbers</a></h3>
<h3 id='18' class='formalized'><a href='http://www.cs.ru.nl/~freek/100/#18'>18. Liouville’s Theorem and the Construction of Transcendental Numbers</a></h3>
<div>

<p class='author'><strong>Valentin Blot</strong>
Expand Down Expand Up @@ -1099,7 +1099,7 @@ <h3 id='52' class='formalized'><a href='http://www.cs.ru.nl/~freek/100/#52'>52.
<p class='axioms'>Axioms used: (none)</p>
<p class='existing'>Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower</p></div>

<h3 id='53' class='formalized'><a href='http://www.cs.ru.nl/~freek/100/#53'>53. Pi is Trancendental</a></h3>
<h3 id='53' class='formalized'><a href='http://www.cs.ru.nl/~freek/100/#53'>53. Pi is Transcendental</a></h3>
<div>

<p class='author'><strong>Sophie Bernard and Laurence Rideau</strong>
Expand Down Expand Up @@ -1632,7 +1632,7 @@ <h3 id='74' class='formalized'><a href='http://www.cs.ru.nl/~freek/100/#74'>74.
<p class='author'><strong>Coq&#039;s type theory</strong>
(in <a href="https://coq.inria.fr/library/Coq.Init.Datatypes.html">coq's standard library</a>):
</p>
<p class='comment'>The induction priciple is automatically provided by Coq when defining unary natural numbers.</p>
<p class='comment'>The induction principle is automatically provided by Coq when defining unary natural numbers.</p>
<pre class='statement'>Inductive nat : Set := O : nat | S : nat -&gt; nat.

nat_ind :
Expand Down
2 changes: 1 addition & 1 deletion statements.yml
Original file line number Diff line number Diff line change
Expand Up @@ -1171,7 +1171,7 @@
- theorem: 74
authors: Coq's type theory
link: https://coq.inria.fr/library/Coq.Init.Datatypes.html
comment: The induction priciple is automatically provided by Coq when defining unary natural numbers.
comment: The induction principle is automatically provided by Coq when defining unary natural numbers.
statement: |
Inductive nat : Set := O : nat | S : nat -> nat.
Expand Down
4 changes: 2 additions & 2 deletions theorems.yml
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@
15: Fundamental Theorem of Integral Calculus
16: Insolvability of General Higher Degree Equations
17: DeMoivre’s Theorem
18: Liouville’s Theorem and the Construction of Trancendental Numbers
18: Liouville’s Theorem and the Construction of Transcendental Numbers
19: Four Squares Theorem
20: All Primes (= 1 mod 4) Equal the Sum of Two Squares
21: Green’s Theorem
Expand Down Expand Up @@ -50,7 +50,7 @@
50: The Number of Platonic Solids
51: Wilson’s Theorem
52: The Number of Subsets of a Set
53: Pi is Trancendental
53: Pi is Transcendental
54: Konigsberg Bridges Problem
55: Product of Segments of Chords
56: The Hermite-Lindemann Transcendence Theorem
Expand Down

0 comments on commit e8bad9f

Please sign in to comment.