# 100 theorems

Freek Wiedijk maintains a list tracking progress of theorem provers in formalizing 100 classic theorems in mathematics as a way of comparing prominent theorem provers. Currently 78 of them are formalized in Lean. We also have a page with the theorems from the list not yet in Lean.

Author: mathlib

##### 2. Fundamental Theorem of Algebra #

Author: Chris Hughes

theorem Complex.exists_root {f : } (hf : 0 < f.degree) :
∃ (z : ), f.IsRoot z
##### 3. The Denumerability of the Rational Numbers #

Author: Chris Hughes

##### 4. Pythagorean Theorem #

Author: Joseph Myers

theorem EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [] [] [] (p1 : P) (p2 : P) (p3 : P) :
dist p1 p3 * dist p1 p3 = dist p1 p2 * dist p1 p2 + dist p3 p2 * dist p3 p2 EuclideanGeometry.angle p1 p2 p3 =
##### 7. Law of Quadratic Reciprocity #

Author: Chris Hughes (first) and Michael Stoll (second)

theorem legendreSym.quadratic_reciprocity {p : } {q : } [Fact p.Prime] [Fact q.Prime] (hp : p 2) (hq : q 2) (hpq : p q) :
legendreSym q p * legendreSym p q = (-1) ^ (p / 2 * (q / 2))
theorem jacobiSym.quadratic_reciprocity {a : } {b : } (ha : Odd a) (hb : Odd b) :
jacobiSym (a) b = (-1) ^ (a / 2 * (b / 2)) * jacobiSym (b) a
##### 9. The Area of a Circle #

Authors: James Arthur, Benjamin Davidson, and Andrew Souther

theorem Theorems100.area_disc (r : NNReal) :
MeasureTheory.volume () = * r ^ 2
##### 10. Euler’s Generalization of Fermat’s Little Theorem #

Author: Chris Hughes

theorem Nat.ModEq.pow_totient {x : } {n : } (h : x.Coprime n) :
n.ModEq (x ^ n.totient) 1
##### 11. The Infinitude of Primes #

theorem Nat.exists_infinite_primes (n : ) :
∃ (p : ), n p p.Prime
##### 14. Euler’s Summation of 1 + (1/2)^2 + (1/3)^2 + …. #

Authors: Marc Masdeu, David Loeffler

theorem hasSum_zeta_two :
HasSum (fun (n : ) => 1 / n ^ 2) ( / 6)
##### 15. Fundamental Theorem of Integral Calculus #

Author: Yury G. Kudryashov (first) and Benjamin Davidson (second)

theorem intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_right {E : Type u_3} [] [] {f : E} {c : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume) (hb : Filter.Tendsto f (nhds b MeasureTheory.volume.ae) (nhds c)) :
HasStrictDerivAt (fun (u : ) => ∫ (x : ) in a..u, f x) c b
theorem intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le {E : Type u_3} [] [] {f : E} {f' : E} {a : } {b : } (hab : a b) (hcont : ContinuousOn f (Set.Icc a b)) (hderiv : xSet.Ioo a b, HasDerivWithinAt f (f' x) () x) (f'int : IntervalIntegrable f' MeasureTheory.volume a b) :
∫ (y : ) in a..b, f' y = f b - f a
##### 16. Insolvability of General Higher Degree Equations (Abel-Ruffini Theorem) #

Author: Thomas Browning

##### 17. De Moivre’s Formula #

Author: Abhimanyu Pallavi Sudhir

theorem Complex.cos_add_sin_mul_I_pow (n : ) (z : ) :
(z.cos + z.sin * Complex.I) ^ n = (n * z).cos + (n * z).sin * Complex.I
##### 18. Liouville’s Theorem and the Construction of Transcendental Numbers #

Author: Jujian Zhang

theorem Liouville.transcendental {x : } (lx : ) :
##### 19. Four Squares Theorem #

Author: Chris Hughes

theorem Nat.sum_four_squares (n : ) :
∃ (a : ) (b : ) (c : ) (d : ), a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n
##### 20. All Primes (1 mod 4) Equal the Sum of Two Squares #

Author: Chris Hughes

theorem Nat.Prime.sq_add_sq {p : } [Fact p.Prime] (hp : p % 4 3) :
∃ (a : ) (b : ), a ^ 2 + b ^ 2 = p
##### 22. The Non-Denumerability of the Continuum #

Author: Floris van Doorn

theorem Cardinal.not_countable_real :
¬Set.univ.Countable
##### 23. Formula for Pythagorean Triples #

Author: Paul van Wamelen

theorem PythagoreanTriple.classification {x : } {y : } {z : } :
∃ (k : ) (m : ) (n : ), (x = k * (m ^ 2 - n ^ 2) y = k * (2 * m * n) x = k * (2 * m * n) y = k * (m ^ 2 - n ^ 2)) (z = k * (m ^ 2 + n ^ 2) z = -k * (m ^ 2 + n ^ 2))
##### 24. The Independence of the Continuum Hypothesis #

Author: Jesse Michael Han and Floris van Doorn

result

website

see the README file in the linked repository.

##### 25. Schroeder-Bernstein Theorem #

Author: Mario Carneiro

theorem Function.Embedding.schroeder_bernstein {α : Type u} {β : Type v} {f : αβ} {g : βα} (hf : ) (hg : ) :
∃ (h : αβ),
##### 26. Leibniz’s Series for Pi #

Author: Benjamin Davidson

theorem Real.tendsto_sum_pi_div_four :
Filter.Tendsto (fun (k : ) => ().sum fun (i : ) => (-1) ^ i / (2 * i + 1)) Filter.atTop (nhds ())
##### 27. Sum of the Angles of a Triangle #

Author: Joseph Myers

theorem EuclideanGeometry.angle_add_angle_add_angle_eq_pi {V : Type u_1} {P : Type u_2} [] [] [] {p1 : P} {p2 : P} {p3 : P} (h2 : p2 p1) (h3 : p3 p1) :
##### 30. The Ballot Problem #

Authors: Bhavik Mehta, Kexing Ying

theorem Ballot.ballot_problem (q : ) (p : ) :
q < p = (p - q) / (p + q)
##### 31. Ramsey’s Theorem #

Author: Bhavik Mehta

result

##### 34. Divergence of the Harmonic Series #

Authors: Anatole Dedecker, Yury Kudryashov

theorem Real.tendsto_sum_range_one_div_nat_succ_atTop :
Filter.Tendsto (fun (n : ) => ().sum fun (i : ) => 1 / (i + 1)) Filter.atTop Filter.atTop
##### 35. Taylor’s Theorem #

Author: Moritz Doll

theorem taylor_mean_remainder_lagrange {f : } {x : } {x₀ : } {n : } (hx : x₀ < x) (hf : ContDiffOn (n) f (Set.Icc x₀ x)) (hf' : DifferentiableOn (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)) :
x'Set.Ioo x₀ x, f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Set.Icc x₀ x) x' * (x - x₀) ^ (n + 1) / (n + 1).factorial
theorem taylor_mean_remainder_cauchy {f : } {x : } {x₀ : } {n : } (hx : x₀ < x) (hf : ContDiffOn (n) f (Set.Icc x₀ x)) (hf' : DifferentiableOn (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)) :
x'Set.Ioo x₀ x, f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Set.Icc x₀ x) x' * (x - x') ^ n / n.factorial * (x - x₀)
##### 36. Brouwer Fixed Point Theorem #

Author: Brendan Seamas Murphy

result

##### 37. The Solution of a Cubic #

Author: Jeoff Lee

theorem Theorems100.cubic_eq_zero_iff {K : Type u_1} [] [] [] (a : K) (b : K) (c : K) (d : K) {ω : K} {p : K} {q : K} {r : K} {s : K} {t : K} (ha : a 0) (hω : ) (hp : p = (3 * a * c - b ^ 2) / (9 * a ^ 2)) (hp_nonzero : p 0) (hq : q = (9 * a * b * c - 2 * b ^ 3 - 27 * a ^ 2 * d) / (54 * a ^ 3)) (hr : r ^ 2 = q ^ 2 + p ^ 3) (hs3 : s ^ 3 = q + r) (ht : t * s = p) (x : K) :
a * x ^ 3 + b * x ^ 2 + c * x + d = 0 x = s - t - b / (3 * a) x = s * ω - t * ω ^ 2 - b / (3 * a) x = s * ω ^ 2 - t * ω - b / (3 * a)
##### 38. Arithmetic Mean/Geometric Mean #

Author: Yury G. Kudryashov

theorem Real.geom_mean_le_arith_mean_weighted {ι : Type u} (s : ) (w : ι) (z : ι) (hw : is, 0 w i) (hw' : (s.sum fun (i : ι) => w i) = 1) (hz : is, 0 z i) :
(s.prod fun (i : ι) => z i ^ w i) s.sum fun (i : ι) => w i * z i
##### 39. Solutions to Pell’s Equation #

Authors: Mario Carneiro (first), Michael Stoll (second)

theorem Pell.eq_pell {a : } (a1 : 1 < a) {x : } {y : } (hp : x * x - Pell.d a1 * y * y = 1) :
∃ (n : ), x = Pell.xn a1 n y = Pell.yn a1 n
theorem Pell.exists_of_not_isSquare {d : } (h₀ : 0 < d) (hd : ) :
∃ (x : ) (y : ), x ^ 2 - d * y ^ 2 = 1 y 0

In pell.eq_pell, d is defined to be a*a - 1 for an arbitrary a > 1.

##### 40. Minkowski’s Fundamental Theorem #

Authors: Alex J. Best, Yaël Dillies

theorem MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure {E : Type u_1} [] {μ : } {F : Set E} {s : Set E} [] [] [] [μ.IsAddHaarMeasure] {L : } [] (fund : ) (h_symm : xs, -x s) (h_conv : ) (h : μ F * < μ s) :
∃ (x : L), x 0 x s
##### 42. Sum of the Reciprocals of the Triangular Numbers #

Authors: Jalex Stark, Yury Kudryashov

theorem Theorems100.inverse_triangle_sum (n : ) :
(().sum fun (k : ) => 2 / (k * (k + 1))) = if n = 0 then 0 else 2 - 2 / n
##### 44. The Binomial Theorem #

Author: Chris Hughes

theorem add_pow {R : Type u_1} [] (x : R) (y : R) (n : ) :
(x + y) ^ n = (Finset.range (n + 1)).sum fun (m : ) => x ^ m * y ^ (n - m) * (n.choose m)
##### 45. The Partition Theorem #

Authors: Bhavik Mehta, Aaron Anderson

theorem Theorems100.partition_theorem (n : ) :
.card = .card
##### 49. The Cayley-Hamilton Theorem #

Author: Scott Morrison

theorem Matrix.aeval_self_charpoly {R : Type u_1} [] {n : Type u_4} [] [] (M : Matrix n n R) :
() M.charpoly = 0
##### 51. Wilson’s Lemma #

Author: Chris Hughes

theorem ZMod.wilsons_lemma (p : ) [Fact p.Prime] :
(p - 1).factorial = -1
##### 52. The Number of Subsets of a Set #

Author: mathlib

theorem Finset.card_powerset {α : Type u_1} (s : ) :
s.powerset.card = 2 ^ s.card
##### 54. Königsberg Bridges Problem #

Author: Kyle Miller

theorem Konigsberg.not_isEulerian {u : Konigsberg.Verts} {v : Konigsberg.Verts} (p : Konigsberg.graph.Walk u v) (h : p.IsEulerian) :
##### 55. Product of Segments of Chords #

Author: Manuel Candales

theorem EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi {V : Type u_1} [] {P : Type u_2} [] [] {a : P} {b : P} {c : P} {d : P} {p : P} (h : EuclideanGeometry.Cospherical {a, b, c, d}) (hapb : ) (hcpd : ) :
dist a p * dist b p = dist c p * dist d p
##### 57. Heron’s Formula #

Author: Matt Kempster

theorem Theorems100.heron {V : Type u_1} {P : Type u_2} [] [] [] {p1 : P} {p2 : P} {p3 : P} (h1 : p1 p2) (h2 : p3 p2) :
let a := dist p1 p2; let b := dist p3 p2; let c := dist p1 p3; let s := (a + b + c) / 2; 1 / 2 * a * b * (EuclideanGeometry.angle p1 p2 p3).sin = (s * (s - a) * (s - b) * (s - c)).sqrt
##### 58. Formula for the Number of Combinations #

Author: mathlib

theorem Finset.card_powersetCard {α : Type u_1} (n : ) (s : ) :
().card = s.card.choose n
theorem Finset.mem_powersetCard {α : Type u_1} {n : } {s : } {t : } :
s s t s.card = n
##### 59. The Laws of Large Numbers #

Author: Sébastien Gouëzel

theorem ProbabilityTheory.strong_law_ae {Ω : Type u_1} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {E : Type u_2} [] [] [] [] (X : ΩE) (hint : MeasureTheory.Integrable (X 0) MeasureTheory.volume) (hindep : Pairwise fun (i j : ) => ProbabilityTheory.IndepFun (X i) (X j) MeasureTheory.volume) (hident : ∀ (i : ), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) :
∀ᵐ (ω : Ω), Filter.Tendsto (fun (n : ) => (n)⁻¹ ().sum fun (i : ) => X i ω) Filter.atTop (nhds (∫ (a : Ω), X 0 a))
##### 60. Bezout’s Theorem #

Author: mathlib

theorem Nat.gcd_eq_gcd_ab (x : ) (y : ) :
(x.gcd y) = x * x.gcdA y + y * x.gcdB y
##### 62. Fair Games Theorem #

Author: Kexing Ying

theorem MeasureTheory.submartingale_iff_expected_stoppedValue_mono {Ω : Type u_1} {m0 : } {μ : } {𝒢 : } {f : Ω} (hadp : ) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) :
∀ (τ π : Ω), τ π(∃ (N : ), ∀ (x : Ω), π x N)∫ (x : Ω), μ ∫ (x : Ω), μ
##### 63. Cantor’s Theorem #

Author: mathlib

theorem Cardinal.cantor (a : Cardinal.{u}) :
a < 2 ^ a
##### 64. L’Hopital’s Rule #

Author: Anatole Dedecker

theorem deriv.lhopital_zero_nhds {a : } {l : } {f : } {g : } (hdf : ∀ᶠ (x : ) in nhds a, ) (hg' : ∀ᶠ (x : ) in nhds a, deriv g x 0) (hfa : Filter.Tendsto f (nhds a) (nhds 0)) (hga : Filter.Tendsto g (nhds a) (nhds 0)) (hdiv : Filter.Tendsto (fun (x : ) => deriv f x / deriv g x) (nhds a) l) :
Filter.Tendsto (fun (x : ) => f x / g x) (nhdsWithin a {a}) l
##### 65. Isosceles Triangle Theorem #

Author: Joseph Myers

theorem EuclideanGeometry.angle_eq_angle_of_dist_eq {V : Type u_1} {P : Type u_2} [] [] [] {p1 : P} {p2 : P} {p3 : P} (h : dist p1 p2 = dist p1 p3) :
##### 66. Sum of a Geometric Series #

Author: Sander R. Dahmen (finite) and Johannes Hölzl (infinite)

theorem geom_sum_Ico {α : Type u} [] {x : α} (hx : x 1) {m : } {n : } (hmn : m n) :
(().sum fun (i : ) => x ^ i) = (x ^ n - x ^ m) / (x - 1)
theorem NNReal.hasSum_geometric {r : NNReal} (hr : r < 1) :
HasSum (fun (n : ) => r ^ n) (1 - r)⁻¹
##### 67. e is Transcendental #

Author: Jujian Zhang

result

website

##### 68. Sum of an arithmetic series #

Author: Johannes Hölzl

theorem Finset.sum_range_id (n : ) :
(().sum fun (i : ) => i) = n * (n - 1) / 2
##### 69. Greatest Common Divisor Algorithm #

Author: mathlib

def EuclideanDomain.gcd {R : Type u} [] [] (a : R) (b : R) :
R
theorem EuclideanDomain.gcd_dvd {R : Type u} [] [] (a : R) (b : R) :
a b
theorem EuclideanDomain.dvd_gcd {R : Type u} [] [] {a : R} {b : R} {c : R} :
c ac bc
##### 70. The Perfect Number Theorem #

Author: Aaron Anderson

theorem Theorems100.Nat.eq_two_pow_mul_prime_mersenne_of_even_perfect {n : } (ev : Even n) (perf : n.Perfect) :
∃ (k : ), (mersenne (k + 1)).Prime n = 2 ^ k * mersenne (k + 1)
##### 71. Order of a Subgroup #

Author: mathlib

theorem Subgroup.card_subgroup_dvd_card {α : Type u_1} [] [] (s : ) [Fintype s] :
##### 72. Sylow’s Theorem #

Author: Chris Hughes

theorem Sylow.exists_subgroup_card_pow_prime {G : Type u} [] [] (p : ) {n : } [Fact p.Prime] (hdvd : p ^ n ) :
∃ (K : ), = p ^ n

sylow_conjugate

card_sylow_dvd

card_sylow_modeq_one

##### 73. Ascending or Descending Sequences (Erdős–Szekeres Theorem) #

Author: Bhavik Mehta

theorem Theorems100.erdos_szekeres {α : Type u_1} [] {r : } {s : } {n : } {f : Fin nα} (hn : r * s < n) (hf : ) :
(∃ (t : Finset (Fin n)), r < t.card StrictMonoOn f t) ∃ (t : Finset (Fin n)), s < t.card StrictAntiOn f t
##### 74. The Principle of Mathematical Induction #

Author: Leonardo de Moura

inductive Nat :

Automatically generated when defining the natural numbers

##### 75. The Mean Value Theorem #

Author: Yury G. Kudryashov

theorem exists_deriv_eq_slope (f : ) {a : } {b : } (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfd : DifferentiableOn f (Set.Ioo a b)) :
cSet.Ioo a b, deriv f c = (f b - f a) / (b - a)
##### 76. Fourier Series #

Author: Heather Macbeth

def fourierCoeff {T : } [hT : Fact (0 < T)] {E : Type} [] (f : E) (n : ) :
E
theorem hasSum_fourier_series_L2 {T : } [hT : Fact (0 < T)] (f : (MeasureTheory.Lp 2 AddCircle.haarAddCircle)) :
HasSum (fun (i : ) => fourierCoeff (f) i ) f
##### 77. Sum of kth powers #

Authors: mathlib (Moritz Firsching, Fabian Kruse, Ashvni Narayanan)

theorem sum_range_pow (n : ) (p : ) :
(().sum fun (k : ) => k ^ p) = (Finset.range (p + 1)).sum fun (i : ) => * ((p + 1).choose i) * n ^ (p + 1 - i) / (p + 1)
theorem sum_Ico_pow (n : ) (p : ) :
((Finset.Ico 1 (n + 1)).sum fun (k : ) => k ^ p) = (Finset.range (p + 1)).sum fun (i : ) => * ((p + 1).choose i) * n ^ (p + 1 - i) / (p + 1)
##### 78. The Cauchy-Schwarz Inequality #

Author: Zhouhang Zhou

theorem inner_mul_inner_self_le {𝕜 : Type u_1} {E : Type u_2} [] [] (x : E) (y : E) :
x, y⟫_𝕜 * y, x⟫_𝕜 RCLike.re x, x⟫_𝕜 * RCLike.re y, y⟫_𝕜
theorem norm_inner_le_norm {𝕜 : Type u_1} {E : Type u_2} [] [] (x : E) (y : E) :
x, y⟫_𝕜 x * y
##### 79. The Intermediate Value Theorem #

Author: mathlib (Rob Lewis and Chris Hughes)

theorem intermediate_value_Icc {α : Type u} [] [] [] {δ : Type u_1} [] [] {a : α} {b : α} (hab : a b) {f : αδ} (hf : ContinuousOn f (Set.Icc a b)) :
Set.Icc (f a) (f b) f '' Set.Icc a b
##### 80. The Fundamental Theorem of Arithmetic #

Author: mathlib (Chris Hughes)

theorem Nat.factors_unique {n : } {l : } (h₁ : l.prod = n) (h₂ : pl, p.Prime) :
l.Perm n.factors
class UniqueFactorizationMonoid (α : Type u_2) extends :
theorem UniqueFactorizationMonoid.factors_unique {α : Type u_1} {f : } {g : } (hf : xf, ) (hg : xg, ) (h : Associated f.prod g.prod) :
Multiset.Rel Associated f g

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.

##### 81. Divergence of the Prime Reciprocal Series #

Authors: Manuel Candales (archive), Michael Stoll (Mathlib)

theorem Theorems100.Real.tendsto_sum_one_div_prime_atTop :
Filter.Tendsto (fun (n : ) => (Finset.filter (fun (p : ) => p.Prime) ()).sum fun (p : ) => 1 / p) Filter.atTop Filter.atTop
theorem not_summable_one_div_on_primes :
¬Summable ({p : | p.Prime}.indicator fun (n : ) => 1 / n)
##### 82. Dissection of Cubes (J.E. Littlewood’s ‘elegant’ proof) #

Author: Floris van Doorn

theorem Theorems100.«82».cannot_cube_a_cube {n : } :
n 3∀ {s : }, s.Finites.Nontrivials.PairwiseDisjoint Theorems100.«82».Cube.toSetcs, c.toSet = Theorems100.«82».Cube.unitCube.toSetSet.InjOn Theorems100.«82».Cube.w sFalse
##### 83. The Friendship Theorem #

Authors: Aaron Anderson, Jalex Stark, Kyle Miller

theorem Theorems100.friendship_theorem {V : Type u} [] {G : } (hG : ) [] :
##### 85. Divisibility by 3 Rule #

Author: Scott Morrison

theorem Nat.three_dvd_iff (n : ) :
3 n 3 (Nat.digits 10 n).sum
##### 86. Lebesgue Measure and Integration #

Author: Johannes Hölzl

def MeasureTheory.lintegral {α : Type u_5} :
{x : } → (αENNReal)ENNReal
##### 88. Derangements Formula #

Author: Henry Swanson

theorem card_derangements_eq_numDerangements (α : Type u_2) [] [] :
theorem numDerangements_sum (n : ) :
() = (Finset.range (n + 1)).sum fun (k : ) => (-1) ^ k * ((k + 1).ascFactorial (n - k))
##### 89. The Factor and Remainder Theorems #

Author: Chris Hughes

theorem Polynomial.dvd_iff_isRoot {R : Type u} {a : R} [] {p : } :
Polynomial.X - Polynomial.C a p p.IsRoot a
theorem Polynomial.mod_X_sub_C_eq_C_eval {R : Type u} [] (p : ) (a : R) :
p % (Polynomial.X - Polynomial.C a) = Polynomial.C ()
##### 90. Stirling’s Formula #

Authors: mathlib (Moritz Firsching, Fabian Kruse, Nikolas Kuhn, Heather Macbeth)

##### 91. The Triangle Inequality #

Author: Zhouhang Zhou

theorem norm_add_le {E : Type u_6} (a : E) (b : E) :
##### 93. The Birthday Problem #

Author: Eric Rodriguez

theorem Theorems100.birthday :
2 * Fintype.card (Fin 23 Fin 365) < Fintype.card (Fin 23Fin 365) 2 * Fintype.card (Fin 22 Fin 365) > Fintype.card (Fin 22Fin 365)
theorem Theorems100.birthday_measure :
MeasureTheory.volume {f : Fin 23Fin 365 | } < 1 / 2
##### 94. The Law of Cosines #

Author: Joseph Myers

theorem EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle {V : Type u_1} {P : Type u_2} [] [] [] (p1 : P) (p2 : P) (p3 : P) :
dist p1 p3 * dist p1 p3 = dist p1 p2 * dist p1 p2 + dist p3 p2 * dist p3 p2 - 2 * dist p1 p2 * dist p3 p2 * (EuclideanGeometry.angle p1 p2 p3).cos
##### 95. Ptolemy’s Theorem #

Author: Manuel Candales

theorem EuclideanGeometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical {V : Type u_1} [] {P : Type u_2} [] [] {a : P} {b : P} {c : P} {d : P} {p : P} (h : EuclideanGeometry.Cospherical {a, b, c, d}) (hapc : ) (hbpd : ) :
dist a b * dist c d + dist b c * dist d a = dist a c * dist b d
##### 96. Principle of Inclusion/Exclusion #

Author: Neil Strickland

github

##### 97. Cramer’s Rule #

Author: Anne Baanen

theorem Matrix.mulVec_cramer {n : Type v} {α : Type w} [] [] [] (A : Matrix n n α) (b : nα) :
A.mulVec (A.cramer b) = A.det b
##### 98. Bertrand’s Postulate #

Authors: Bolton Bailey, Patrick Stevens

theorem Nat.bertrand (n : ) (hn0 : n 0) :
∃ (p : ), p.Prime n < p p 2 * n
##### 99. Buffon Needle Problem #

Author: Enrico Z. Borba

theorem BuffonsNeedle.buffon_short {Ω : Type u_1} (d : ) (l : ) (hd : 0 < d) (hl : 0 < l) (B : Ω) (hBₘ : ) (hB : MeasureTheory.pdf.IsUniform B (Set.Icc (-d / 2) (d / 2) ×ˢ ) MeasureTheory.volume MeasureTheory.volume) (h : l d) :
∫ (x : Ω), = 2 * l * ()⁻¹
theorem BuffonsNeedle.buffon_long {Ω : Type u_1} (d : ) (l : ) (hd : 0 < d) (hl : 0 < l) (B : Ω) (hBₘ : ) (hB : MeasureTheory.pdf.IsUniform B (Set.Icc (-d / 2) (d / 2) ×ˢ ) MeasureTheory.volume MeasureTheory.volume) (h : d l) :
∫ (x : Ω), = 2 * l / () - 2 / () * ((l ^ 2 - d ^ 2).sqrt + d * (d / l).arcsin) + 1
##### 100. Descartes Rule of Signs #

Author: Alex Meiburg

github