freek.yaml, initial version

freek.yaml

freek:
   1:
      - title  : The Irrationality of the Square Root of 2
      - decl   : irr_sqrt_two
      - author : mathlib
   2:
      - title  : Fundamental Theorem of Algebra
      - decl   : exists_root
      - author : Chris Hughes
   3:
      - title  : The Denumerability of the Rational Numbers
      - decl   :
      - author : Chris Hughes
   4:
      - title  : Pythagorean Theorem
      - decl   :
      - author :
   5:
      - title  : Prime Number Theorem
      - author :
   6:
      - title  : Godel’s Incompleteness Theorem
      - decl   :
      - author :
   7:
      - title  : Law of Quadratic Reciprocity
      - decl   : quadratic_reciprocity
      - author : Chris Hughes
   8:
      - title  : The Impossibility of Trisecting the Angle and Doubling the Cube
      - author :
   9:
      - title  : The Area of a Circle
      - author :
   10:
      - title  : Euler’s Generalization of Fermat’s Little Theorem
      - author :
   11:
      - title  : The Infinitude of Primes
      - decl   : exists_infinite_primes
      - author : Jeremy Avigad
   12:
      - title  : The Independence of the Parallel Postulate
      - author :
   13:
      - title  : Polyhedron Formula
      - author :
   14:
      - title  : Euler’s Summation of 1 + (1/2)^2 + (1/3)^2 + ….
      - author :
   15:
      - title  : Fundamental Theorem of Integral Calculus
      - author :
   16:
      - title  : Insolvability of General Higher Degree Equations
      - author :
   17:
      - title  : De Moivre’s Theorem
      - decl   : 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
      - author : Chris Hughes
   20:
      - title  : All Primes (1 mod 4) Equal the Sum of Two Squares
      - decl   : sum_two_squares
      - author : Chris Hughes
   21:
      - title  : Green’s Theorem
      - author :
   22:
      - title  : The Non-Denumerability of the Continuum
      - decl   : not_countable_real
      - author : Floris van Doorn
   23:
      - title  : Formula for Pythagorean Triples
      - author :
   24:
      - title  : The Undecidability of the Continuum Hypothesis
      - decl   : independence_of_CH
      - author : Jesse Michael Han and Floris van Doorn
      - link   : [result](https://github.com/flypitch/flypitch/), [website](https://flypitch.github.io/)
      - note   : see the `README` file in the linked repository.
   25:
      - title  : Schroeder-Bernstein Theorem
      - decl   : schroeder_bernstein
      - author : Mario Carneiro
   26:
      - title  : Leibnitz’s Series for Pi
      - author :
   27:
      - title  : Sum of the Angles of a Triangle
      - author :
   28:
      - title  : Pascal’s Hexagon Theorem
      - author :
   29:
      - title  : Feuerbach’s Theorem
      - author :
   30:
      - title  : The Ballot Problem
      - author :
   31:
      - title  : Ramsey’s Theorem
      - author :
   32:
      - title  : The Four Color Problem
      - author :
   33:
      - title  : Fermat’s Last Theorem
      - author :
   34:
      - title  : Divergence of the Harmonic Series
      - author :
   35:
      - title  : Taylor’s Theorem
      - author :
   36:
      - title  : Brouwer Fixed Point Theorem
      - author :
   37:
      - title  : The Solution of a Cubic
      - author :
   38:
      - title  : Arithmetic Mean/Geometric Mean
      - decl   : real.am_gm_weighted
      - author : mathlib
   39:
      - title  : Solutions to Pell’s Equation
      - decl   : eq_pell
      - author : Mario Carneiro
      - note   : `d` is defined to be `a*a - 1` for an arbitrary `a > 1`.
   40:
      - title  : Minkowski’s Fundamental Theorem
      - author :
   41:
      - title  : Puiseux’s Theorem
      - author :
   42:
      - title  : Sum of the Reciprocals of the Triangular Numbers
      - author :
   43:
      - title  : The Isoperimetric Theorem
      - author :
   44:
      - title  : The Binomial Theorem
      - decl   : add_pow
      - author : Chris Hughes
   45:
      - title  : The Partition Theorem
      - author :
   46:
      - title  : The Solution of the General Quartic Equation
      - author :
   47:
      - title  : The Central Limit Theorem
      - author :
   48:
      - title  : Dirichlet’s Theorem
      - author :
   49:
      - title  : The Cayley-Hamilton Thoerem
      - author :
   50:
      - title  : The Number of Platonic Solids
      - author :
   51:
      - title  : Wilson’s Theorem
      - decl   : wilsons_lemma
      - author : Chris Hughes
   52:
      - title  : The Number of Subsets of a Set
      - decl   : card_powerset
      - author : mathlib
   53:
      - title  : Pi is Trancendental
      - author :
   54:
      - title  : Konigsberg Bridges Problem
      - author :
   55:
      - title  : Product of Segments of Chords
      - author :
   56:
      - title  : The Hermite-Lindemann Transcendence Theorem
      - author :
   57:
      - title  : Heron’s Formula
      - author :
   58:
      - title  : Formula for the Number of Combinations
      - decl   : [card_powerset_len, 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
      - author : mathlib
   61:
      - title  : Theorem of Ceva
      - author :
   62:
      - title  : Fair Games Theorem
      - author :
   63:
      - title  : Cantor’s Theorem
      - decl   : cantor
      - author : mathlib <!-- Mario and/or Johannes -->
   64:
      - title  : L’Hopital’s Rule
      - author :
   65:
      - title  : Isosceles Triangle Theorem
      - author :
   66:
      - title  : Sum of a Geometric Series
      - decl   : [geom_sum, 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
      - author : Johannes Hölzl
   69:
      - title  : Greatest Common Divisor Algorithm
      - decl   : [gcd, gcd_dvd, dvd_gcd]
   ```
      - author : mathlib
   70:
      - title  : The Perfect Number Theorem
      - author :
   71:
      - title  : Order of a Subgroup
      - decl   : 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]
      - author : Chris Hughes
   73:
      - title  : Ascending or Descending Sequences
      - author :
   74:
      - title  : The Principle of Mathematical Induction
      - decl   : [nat, nat.rec]
      - note   : Automatically generated when defining the natural numbers
      - author : Leonardo de Moura
   75:
      - title  : The Mean Value Theorem
      - author :
   76:
      - title  : Fourier Series
      - author :
   77:
      - title  : Sum of kth powers
      - author :
   78:
      - title  : The Cauchy-Schwarz Inequality
      - author :
   79:
      - title  : The Intermediate Value Theorem
      - decl   : real
      - author : mathlib (Rob Lewis and Chris Hughes)
   80:
      - title  : The Fundamental Theorem of Arithmetic
      - decl   : 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)
   81:
      - title  : Divergence of the Prime Reciprocal Series
      - author :
   82:
      - title  : Dissection of Cubes (J.E. Littlewood’s ‘elegant’ proof)
      - decl   : cannot_cube_a_cube
      - author : Floris van Doorn
   83:
      - title  : The Friendship Theorem
      - author :
   84:
      - title  : Morley’s Theorem
      - author :
   85:
      - title  : Divisibility by 3 Rule
      - author :
   86:
      - title  : Lebesgue Measure and Integration
      - decl   : lintegral
      - author : Johannes Hölzl
   87:
      - title  : Desargues’s Theorem
      - author :
   88:
      - title  : Derangements Formula
      - author :
   89:
      - title  : The Factor and Remainder Theorems
      - decl   : [dvd_iff_is_root, mod_X_sub_C_eq_C_eval]
      - author : Chris Hughes
   90:
      - title  : Stirling’s Formula
      - author :
   91:
      - title  : The Triangle Inequality
      - author :
   92:
      - title  : Pick’s Theorem
      - author :
   93:
      - title  : The Birthday Problem
      - author :
   94:
      - title  : The Law of Cosines
      - author :
   95:
      - title  : Ptolemy’s Theorem
      - author :
   96:
      - title  : Principle of Inclusion/Exclusion
      - decl   : inclusion_exclusion
      - author : Neil Strickland
   97:
      - title  : Cramer’s Rule
      - author :
   98:
      - title  : Bertrand’s Postulate
      - author :
   99:
      - title  : Buffon Needle Problem
      - author :
   100:
      - title  : Descartes Rule of Signs
      - author :