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.

Sign up for GitHub

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

Jump to bottom

add full links to freek.yaml #16

Merged
merged 3 commits into from
May 15, 2020
Merged

add full links to freek.yaml #16

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
979e123
add full links
jalex-stark May 15, 2020
0dc9ad8
Update data/100.yaml
jalex-stark May 15, 2020
1a67126
Update data/100.yaml
jalex-stark May 15, 2020
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
54 changes: 27 additions & 27 deletions data/100.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,11 @@
100thms:
1:
- title : The Irrationality of the Square Root of 2
- decl : irr_sqrt_two
- decl : data/real/irrational.html#irrational_sqrt_two
- author : mathlib
2:
- title : Fundamental Theorem of Algebra
- decl : exists_root
- decl : analysis/complex/polynomial.html#complex.exists_root
- author : Chris Hughes
3:
- title : The Denumerability of the Rational Numbers
Expand All @@ -24,7 +24,7 @@
- author :
7:
- title : Law of Quadratic Reciprocity
- decl : quadratic_reciprocity
- decl : number_theory.quadratic_reciprocity.html#zmod.quadratic_reciprocity
- author : Chris Hughes
8:
- title : The Impossibility of Trisecting the Angle and Doubling the Cube
Expand All @@ -37,7 +37,7 @@
- author :
11:
- title : The Infinitude of Primes
- decl : exists_infinite_primes
- decl : data.nat.prime.html#nat.exists_infinite_primes
- author : Jeremy Avigad
12:
- title : The Independence of the Parallel Postulate
Expand All @@ -56,25 +56,25 @@
- author :
17:
- title : De Moivre’s Theorem
- decl : cos_add_sin_mul_I_pow
- decl : data.complex.exponential.html#complex.cos_add_sin_mul_I_pow
- author : mathlib
18:
- title : Liouville’s Theorem and the Construction of Trancendental Numbers
- author :
19:
- title : Four Squares Theorem
- decl : sum_four_squares
- decl : number_theory.sum_four_squares.html#nat.sum_four_squares
- author : Chris Hughes
20:
- title : All Primes (1 mod 4) Equal the Sum of Two Squares
- decl : sum_two_squares
- decl : field_theory.finite.html#zmod.sum_two_squares
- author : Chris Hughes
21:
- title : Green’s Theorem
- author :
22:
- title : The Non-Denumerability of the Continuum
- decl : not_countable_real
- decl : data/real/cardinality.html#cardinal.not_countable_real
- author : Floris van Doorn
23:
- title : Formula for Pythagorean Triples
Expand All @@ -87,7 +87,7 @@
- note : see the `README` file in the linked repository.
25:
- title : Schroeder-Bernstein Theorem
- decl : schroeder_bernstein
- decl : set_theory.schroeder_bernstein.html#function.embedding.schroeder_bernstein
- author : Mario Carneiro
26:
- title : Leibnitz’s Series for Pi
Expand Down Expand Up @@ -127,11 +127,11 @@
- author :
38:
- title : Arithmetic Mean/Geometric Mean
- decl : real.am_gm_weighted
- decl : analysis/mean_inequalities.html#real.am_gm_weighted
- author : mathlib
39:
- title : Solutions to Pell’s Equation
- decl : eq_pell
- decl : number_theory/pell.html#pell.eq_pell
- author : Mario Carneiro
- note : `d` is defined to be `a*a - 1` for an arbitrary `a > 1`.
40:
Expand All @@ -148,7 +148,7 @@
- author :
44:
- title : The Binomial Theorem
- decl : add_pow
- decl : data/nat/choose.html#add_pow
- author : Chris Hughes
45:
- title : The Partition Theorem
Expand All @@ -170,11 +170,11 @@
- author :
51:
- title : Wilson’s Theorem
- decl : wilsons_lemma
- decl : number_theory/quadratic_reciprocity.html#zmod.wilsons_lemma
- author : Chris Hughes
52:
- title : The Number of Subsets of a Set
- decl : card_powerset
- decl : data/finset.html#finset.card_powerset
- author : mathlib
53:
- title : Pi is Trancendental
Expand All @@ -193,14 +193,14 @@
- author :
58:
- title : Formula for the Number of Combinations
- decl : [card_powerset_len, mem_powerset_len]
- decl : [data/finset.html#finset.card_powerset_len, data/finset.html#finset.mem_powerset_len]
- author : mathlib <!--Jeremy Avigad in lean 2-->
59:
- title : The Laws of Large Numbers
- author :
60:
- title : Bezout’s Theorem
- decl : gcd_eq_gcd_ab
- decl : data/int/gcd.html#nat.gcd_eq_gcd_ab
- author : mathlib
61:
- title : Theorem of Ceva
Expand All @@ -210,7 +210,7 @@
- author :
63:
- title : Cantor’s Theorem
- decl : cantor
- decl : set_theory/cardinal.html#cardinal.cantor
- author : mathlib <!-- Mario and/or Johannes -->
64:
- title : L’Hopital’s Rule
Expand All @@ -220,29 +220,29 @@
- author :
66:
- title : Sum of a Geometric Series
- decl : [geom_sum, has_sum_geometric]
- decl : [algebra/geom_sum.html#geom_sum, analysis/specific_limits.html#nnreal.has_sum_geometric]
- author : Sander R. Dahmen (finite) and Johannes Hölzl (infinite)
67:
- title : e is Transcendental
- author :
68:
- title : Sum of an arithmetic series
- decl : sum_range_id
- decl : algebra/big_operators.html#finset.sum_range_id
- author : Johannes Hölzl
69:
- title : Greatest Common Divisor Algorithm
- decl : [gcd, gcd_dvd, dvd_gcd]
- decl : [algebra/euclidean_domain.html#euclidean_domain.gcd, algebra/euclidean_domain.html#euclidean_domain.gcd_dvd, algebra/euclidean_domain.html#euclidean_domain.dvd_gcd]
- author : mathlib
70:
- title : The Perfect Number Theorem
- author :
71:
- title : Order of a Subgroup
- decl : card_subgroup_dvd_card
- decl : group_theory/order_of_element.html#card_subgroup_dvd_card
- author : mathlib
72:
- title : Sylow’s Theorem
- decl : [exists_subgroup_card_pow_prime, sylow_conjugate, card_sylow_dvd, card_sylow_modeq_one]
- decl : [group_theory/sylow.html#sylow.exists_subgroup_card_pow_prime, group_theory/sylow.html#sylow_conjugate, group_theory/sylow.html#card_sylow_dvd, group_theory/sylow.html#card_sylow_modeq_one]
- author : Chris Hughes
73:
- title : Ascending or Descending Sequences
Expand All @@ -254,7 +254,7 @@
- author : Leonardo de Moura
75:
- title : The Mean Value Theorem
- decl : exists_deriv_eq_slope
- decl : analysis/calculus/mean_value.html#exists_deriv_eq_slope
- author : mathlib
76:
- title : Fourier Series
Expand All @@ -271,7 +271,7 @@
- author : mathlib (Rob Lewis and Chris Hughes)
80:
- title : The Fundamental Theorem of Arithmetic
- decl : factors_unique
- decl : data/nat/prime.html#nat.factors_unique
- author : mathlib (Chris Hughes)
- note |
it also has a generalized version, by showing that every Euclidean domain is a unique factorization domain, and showing that the integers form a Euclidean domain. Links: [1](https://github.com/leanprover-community/mathlib/blob/4845b663c182704738868db5861ffb4c6056be23/src/algebra/euclidean_domain.lean#L320) [2](https://github.com/leanprover-community/mathlib/blob/4845b663c182704738868db5861ffb4c6056be23/src/ring_theory/principal_ideal_domain.lean#L71) [3](https://github.com/leanprover-community/mathlib/blob/4845b663c182704738868db5861ffb4c6056be23/src/ring_theory/principal_ideal_domain.lean#L158) [4](https://github.com/leanprover-community/mathlib/blob/4845b663c182704738868db5861ffb4c6056be23/src/ring_theory/unique_factorization_domain.lean#L29) [5](https://github.com/leanprover-community/mathlib/blob/master/src/ring_theory/unique_factorization_domain.lean#L90)
Expand All @@ -280,7 +280,7 @@ it also has a generalized version, by showing that every Euclidean domain is a u
- author :
82:
- title : Dissection of Cubes (J.E. Littlewood’s ‘elegant’ proof)
- decl : cannot_cube_a_cube
- decl : archive/cubing_a_cube.html#cannot_cube_a_cube
- author : Floris van Doorn
83:
- title : The Friendship Theorem
Expand All @@ -293,7 +293,7 @@ it also has a generalized version, by showing that every Euclidean domain is a u
- author :
86:
- title : Lebesgue Measure and Integration
- decl : lintegral
- decl : measure_theory/integration.html#measure_theory.lintegral
- author : Johannes Hölzl
87:
- title : Desargues’s Theorem
Expand All @@ -303,7 +303,7 @@ it also has a generalized version, by showing that every Euclidean domain is a u
- author :
89:
- title : The Factor and Remainder Theorems
- decl : [dvd_iff_is_root, mod_X_sub_C_eq_C_eval]
- decl : [data/polynomial.html#polynomial.dvd_iff_is_root, data/polynomial.html#polynomial.mod_X_sub_C_eq_C_eval]
- author : Chris Hughes
90:
- title : Stirling’s Formula
Expand Down