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 81 of them are formalized in Lean. We also have a page with the theorems from the list not yet in Lean.

To make updates to this list, please make a pull request to mathlib after editing the yaml source file. This can be done entirely on GitHub, see "Editing files in another user's repository".

1. The Irrationality of the Square Root of 2 #

Author: mathlib

theorem irrational_sqrt_two :
Irrational √2

docs, source

2. Fundamental Theorem of Algebra #

Author: Chris Hughes

theorem Complex.exists_root {f : Polynomial ℂ} (hf : 0 < f.degree) :
∃ (z : ℂ), f.IsRoot z

docs, source

3. The Denumerability of the Rational Numbers #

Author: Chris Hughes

instance Rat.instDenumerable :
Denumerable ℚ

docs, source

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p1 p2 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 = Real.pi / 2

docs, source

6. Gödel’s Incompleteness Theorem #

Author: Shogo Saito

results

website

7. Law of Quadratic Reciprocity #

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

theorem legendreSym.quadratic_reciprocity {p q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] (hp : p ≠ 2) (hq : q ≠ 2) (hpq : p ≠ q) :
legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))

docs, source

theorem jacobiSym.quadratic_reciprocity {a b : ℕ} (ha : Odd a) (hb : Odd b) :
jacobiSym (↑a) b = (-1) ^ (a / 2 * (b / 2)) * jacobiSym (↑b) a

docs, source

9. The Area of a Circle #

Authors: James Arthur and Benjamin Davidson and Andrew Souther

theorem Theorems100.area_disc (r : NNReal) :
MeasureTheory.volume (Theorems100.disc ↑r) = ↑NNReal.pi * ↑r ^ 2

docs, source

10. Euler’s Generalization of Fermat’s Little Theorem #

Author: Chris Hughes

theorem Nat.ModEq.pow_totient {x n : ℕ} (h : x.Coprime n) :
x ^ n.totient ≡ 1 [MOD n]

docs, source

11. The Infinitude of Primes #

Author: Jeremy Avigad

theorem Nat.exists_infinite_primes (n : ℕ) :
∃ (p : ℕ), n ≤ p ∧ Nat.Prime p

docs, source

14. Euler’s Summation of 1 + (1/2)^2 + (1/3)^2 + …. #

Authors: Marc Masdeu and David Loeffler

theorem hasSum_zeta_two :
HasSum (fun (n : ℕ) => 1 / ↑n ^ 2) (Real.pi ^ 2 / 6)

docs, source

15. Fundamental Theorem of Integral Calculus #

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

theorem intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_right {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {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.ae MeasureTheory.volume) (nhds c)) :
HasStrictDerivAt (fun (u : ℝ) => ∫ (x : ℝ) in a..u, f x) c b

docs, source

theorem intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f f' : ℝ → E} (hab : a ≤ b) (hcont : ContinuousOn f (Set.Icc a b)) (hderiv : ∀ x ∈ Set.Ioo a b, HasDerivWithinAt f (f' x) (Set.Ioi x) x) (f'int : IntervalIntegrable f' MeasureTheory.volume a b) :
∫ (y : ℝ) in a..b, f' y = f b - f a

docs, source

16. Insolvability of General Higher Degree Equations (Abel-Ruffini Theorem) #

Author: Thomas Browning

theorem AbelRuffini.exists_not_solvable_by_rad :
∃ (x : ℂ), IsAlgebraic ℚ x ∧ ¬IsSolvableByRad ℚ x

docs, source

17. De Moivre’s Formula #

Author: Abhimanyu Pallavi Sudhir

theorem Complex.cos_add_sin_mul_I_pow (n : ℕ) (z : ℂ) :
(Complex.cos z + Complex.sin z * Complex.I) ^ n = Complex.cos (↑n * z) + Complex.sin (↑n * z) * Complex.I

docs, source

18. Liouville’s Theorem and the Construction of Transcendental Numbers #

Author: Jujian Zhang

theorem Liouville.transcendental {x : ℝ} (lx : Liouville x) :
Transcendental ℤ x

docs, source

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

docs, source

20. All Primes (1 mod 4) Equal the Sum of Two Squares #

Author: Chris Hughes

theorem Nat.Prime.sq_add_sq {p : ℕ} [Fact (Nat.Prime p)] (hp : p % 4 ≠ 3) :
∃ (a : ℕ) (b : ℕ), a ^ 2 + b ^ 2 = p

docs, source

22. The Non-Denumerability of the Continuum #

Author: Floris van Doorn

theorem Cardinal.not_countable_real :
¬Set.univ.Countable

docs, source

23. Formula for Pythagorean Triples #

Author: Paul van Wamelen

theorem PythagoreanTriple.classification {x y z : ℤ} :
PythagoreanTriple 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))

docs, source

24. The Independence of the Continuum Hypothesis #

Authors: 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 : Function.Injective f) (hg : Function.Injective g) :
∃ (h : α → β), Function.Bijective h

docs, source

26. Leibniz’s Series for Pi #

Author: Benjamin Davidson

theorem Real.tendsto_sum_pi_div_four :
Filter.Tendsto (fun (k : ℕ) => ∑ i ∈ Finset.range k, (-1) ^ i / (2 * ↑i + 1)) Filter.atTop (nhds (Real.pi / 4))

docs, source

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p1 p2 p3 : P} (h2 : p2 ≠ p1) (h3 : p3 ≠ p1) :
EuclideanGeometry.angle p1 p2 p3 + EuclideanGeometry.angle p2 p3 p1 + EuclideanGeometry.angle p3 p1 p2 = Real.pi

docs, source

30. The Ballot Problem #

Authors: Bhavik Mehta and Kexing Ying

theorem Ballot.ballot_problem (q p : ℕ) :
q < p → (ProbabilityTheory.uniformOn (Ballot.countedSequence p q)) Ballot.staysPositive = (↑p - ↑q) / (↑p + ↑q)

docs, source

31. Ramsey’s Theorem #

Author: Bhavik Mehta

result

34. Divergence of the Harmonic Series #

Authors: Anatole Dedecker and Yury Kudryashov

theorem Real.tendsto_sum_range_one_div_nat_succ_atTop :
Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, 1 / (↑i + 1)) Filter.atTop Filter.atTop

docs, source

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

docs, source

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₀)

docs, source

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} [Field K] (a b c d : K) {ω p q r s t : K} [Invertible 2] [Invertible 3] (ha : a ≠ 0) (hω : IsPrimitiveRoot ω 3) (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)

docs, source

38. Arithmetic Mean/Geometric Mean #

Author: Yury G. Kudryashov

theorem Real.geom_mean_le_arith_mean_weighted {ι : Type u} (s : Finset ι) (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) :
∏ i ∈ s, z i ^ w i ≤ ∑ i ∈ s, w i * z i

docs, source

39. Solutions to Pell’s Equation #

Author: 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

docs, source

theorem Pell.exists_of_not_isSquare {d : ℤ} (h₀ : 0 < d) (hd : ¬IsSquare d) :
∃ (x : ℤ) (y : ℤ), x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0

docs, source

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 and Yaël Dillies

theorem MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {F s : Set E} [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {L : AddSubgroup E} [Countable ↥L] (fund : MeasureTheory.IsAddFundamentalDomain (↥L) F μ) (h_symm : ∀ x ∈ s, -x ∈ s) (h_conv : Convex ℝ s) (h : μ F * 2 ^ Module.finrank ℝ E < μ s) :
∃ (x : ↥L), x ≠ 0 ∧ ↑x ∈ s

docs, source

42. Sum of the Reciprocals of the Triangular Numbers #

Authors: Jalex Stark and Yury Kudryashov

theorem Theorems100.inverse_triangle_sum (n : ℕ) :
∑ k ∈ Finset.range n, 2 / (↑k * (↑k + 1)) = if n = 0 then 0 else 2 - 2 / ↑n

docs, source

44. The Binomial Theorem #

Author: Chris Hughes

theorem add_pow {R : Type u_1} [CommSemiring R] (x y : R) (n : ℕ) :
(x + y) ^ n = ∑ m ∈ Finset.range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)

docs, source

45. The Partition Theorem #

Authors: Bhavik Mehta and Aaron Anderson

theorem Theorems100.partition_theorem (n : ℕ) :
(Nat.Partition.odds n).card = (Nat.Partition.distincts n).card

docs, source

46. The Solution of the General Quartic Equation #

Author: Thomas Zhu

theorem Theorems100.quartic_eq_zero_iff {K : Type u_1} [Field K] (a b c d e : K) {p q r s u v w : K} [Invertible 2] (ha : a ≠ 0) (hp : p = (8 * a * c - 3 * b ^ 2) / (8 * a ^ 2)) (hq : q = (b ^ 3 - 4 * a * b * c + 8 * a ^ 2 * d) / (8 * a ^ 3)) (hq_nonzero : q ≠ 0) (hr : r = (16 * a * b ^ 2 * c + 256 * a ^ 3 * e - 3 * b ^ 4 - 64 * a ^ 2 * b * d) / (256 * a ^ 4)) (hu : u ^ 3 - p * u ^ 2 - 4 * r * u + 4 * p * r - q ^ 2 = 0) (hs : s ^ 2 = u - p) (hv : v ^ 2 = 4 * s ^ 2 - 8 * (u - q / s)) (hw : w ^ 2 = 4 * s ^ 2 - 8 * (u + q / s)) (x : K) :
a * x ^ 4 + b * x ^ 3 + c * x ^ 2 + d * x + e = 0 ↔ x = (-2 * s - v) / 4 - b / (4 * a) ∨ x = (-2 * s + v) / 4 - b / (4 * a) ∨ x = (2 * s - w) / 4 - b / (4 * a) ∨ x = (2 * s + w) / 4 - b / (4 * a)

docs, source

48. Dirichlet’s Theorem #

Author: David Loeffler, Michael Stoll

theorem Nat.setOf_prime_and_eq_mod_infinite {q : ℕ} [NeZero q] {a : ZMod q} (ha : IsUnit a) :
{p : ℕ | Nat.Prime p ∧ ↑p = a}.Infinite

docs, source

49. The Cayley-Hamilton Theorem #

Author: Kim Morrison

theorem Matrix.aeval_self_charpoly {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] (M : Matrix n n R) :
(Polynomial.aeval M) M.charpoly = 0

docs, source

51. Wilson’s Lemma #

Author: Chris Hughes

theorem ZMod.wilsons_lemma (p : ℕ) [Fact (Nat.Prime p)] :
↑(p - 1).factorial = -1

docs, source

52. The Number of Subsets of a Set #

Author: mathlib

theorem Finset.card_powerset {α : Type u_1} (s : Finset α) :
s.powerset.card = 2 ^ s.card

docs, source

54. Königsberg Bridges Problem #

Author: Kyle Miller

theorem Konigsberg.not_isEulerian {u v : Konigsberg.Verts} (p : Konigsberg.graph.Walk u v) (h : p.IsEulerian) :
False

docs, source

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {P : Type u_2} [MetricSpace P] [NormedAddTorsor V P] {a b c d p : P} (h : EuclideanGeometry.Cospherical {a, b, c, d}) (hapb : EuclideanGeometry.angle a p b = Real.pi) (hcpd : EuclideanGeometry.angle c p d = Real.pi) :
dist a p * dist b p = dist c p * dist d p

docs, source

57. Heron’s Formula #

Author: Matt Kempster

theorem Theorems100.heron {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p1 p2 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 * Real.sin (EuclideanGeometry.angle p1 p2 p3) = √(s * (s - a) * (s - b) * (s - c))

docs, source

58. Formula for the Number of Combinations #

Author: mathlib

theorem Finset.card_powersetCard {α : Type u_1} (n : ℕ) (s : Finset α) :
(Finset.powersetCard n s).card = s.card.choose n

docs, source

theorem Finset.mem_powersetCard {α : Type u_1} {n : ℕ} {s t : Finset α} :
s ∈ Finset.powersetCard n t ↔ s ⊆ t ∧ s.card = n

docs, source

59. The Laws of Large Numbers #

Author: Sébastien Gouëzel

theorem ProbabilityTheory.strong_law_ae {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] (X : ℕ → Ω → E) (hint : MeasureTheory.Integrable (X 0) μ) (hindep : Pairwise ((fun (x1 x2 : Ω → E) => ProbabilityTheory.IndepFun x1 x2 μ) on X)) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) :
∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) Filter.atTop (nhds (∫ (x : Ω), X 0 x ∂μ))

docs, source

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

docs, source

62. Fair Games Theorem #

Author: Kexing Ying

theorem MeasureTheory.submartingale_iff_expected_stoppedValue_mono {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0} {f : ℕ → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hadp : MeasureTheory.Adapted 𝒢 f) (hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) :
MeasureTheory.Submartingale f 𝒢 μ ↔ ∀ (τ π : Ω → ℕ), MeasureTheory.IsStoppingTime 𝒢 τ → MeasureTheory.IsStoppingTime 𝒢 π → τ ≤ π → (∃ (N : ℕ), ∀ (x : Ω), π x ≤ N) → ∫ (x : Ω), MeasureTheory.stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), MeasureTheory.stoppedValue f π x ∂μ

docs, source

63. Cantor’s Theorem #

Authors: Johannes Hölzl and Mario Carneiro

theorem Function.cantor_surjective {α : Type u_4} (f : α → Set α) :
¬Function.Surjective f

docs, source

64. L’Hopital’s Rule #

Author: Anatole Dedecker

theorem deriv.lhopital_zero_nhds {a : ℝ} {l : Filter ℝ} {f g : ℝ → ℝ} (hdf : ∀ᶠ (x : ℝ) in nhds a, DifferentiableAt ℝ f x) (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

docs, source

65. Isosceles Triangle Theorem #

Author: Joseph Myers

theorem EuclideanGeometry.angle_eq_angle_of_dist_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p1 p2 p3 : P} (h : dist p1 p2 = dist p1 p3) :
EuclideanGeometry.angle p1 p2 p3 = EuclideanGeometry.angle p1 p3 p2

docs, source

66. Sum of a Geometric Series #

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

theorem geom_sum_Ico {α : Type u} [DivisionRing α] {x : α} (hx : x ≠ 1) {m n : ℕ} (hmn : m ≤ n) :
∑ i ∈ Finset.Ico m n, x ^ i = (x ^ n - x ^ m) / (x - 1)

docs, source

theorem NNReal.hasSum_geometric {r : NNReal} (hr : r < 1) :
HasSum (fun (n : ℕ) => r ^ n) (1 - r)⁻¹

docs, source

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 : ℕ) :
∑ i ∈ Finset.range n, i = n * (n - 1) / 2

docs, source

69. Greatest Common Divisor Algorithm #

Author: mathlib

def EuclideanDomain.gcd {R : Type u} [EuclideanDomain R] [DecidableEq R] (a b : R) :
R

docs, source

theorem EuclideanDomain.gcd_dvd {R : Type u} [EuclideanDomain R] [DecidableEq R] (a b : R) :
EuclideanDomain.gcd a b ∣ a ∧ EuclideanDomain.gcd a b ∣ b

docs, source

theorem EuclideanDomain.dvd_gcd {R : Type u} [EuclideanDomain R] [DecidableEq R] {a b c : R} :
c ∣ a → c ∣ b → c ∣ EuclideanDomain.gcd a b

docs, source

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 : ℕ), Nat.Prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1)

docs, source

71. Order of a Subgroup #

Author: mathlib

theorem Subgroup.card_subgroup_dvd_card {α : Type u_1} [Group α] (s : Subgroup α) :
Nat.card ↥s ∣ Nat.card α

docs, source

72. Sylow’s Theorem #

Author: Chris Hughes

theorem Sylow.exists_subgroup_card_pow_prime {G : Type u} [Group G] [Finite G] (p : ℕ) {n : ℕ} [Fact (Nat.Prime p)] (hdvd : p ^ n ∣ Nat.card G) :
∃ (K : Subgroup G), Nat.card ↥K = p ^ n

docs, source

instance Sylow.isPretransitive_of_finite {p : ℕ} {G : Type u_1} [Group G] [hp : Fact (Nat.Prime p)] [Finite (Sylow p G)] :
MulAction.IsPretransitive G (Sylow p G)

docs, source

theorem Sylow.card_dvd_index {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) :
Nat.card (Sylow p G) ∣ (↑P).index

docs, source

theorem card_sylow_modEq_one (p : ℕ) (G : Type u_1) [Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] :
Nat.card (Sylow p G) ≡ 1 [MOD p]

docs, source

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

Author: Bhavik Mehta

theorem Theorems100.erdos_szekeres {α : Type u_1} [LinearOrder α] {r s n : ℕ} {f : Fin n → α} (hn : r * s < n) (hf : Function.Injective f) :
(∃ (t : Finset (Fin n)), r < t.card ∧ StrictMonoOn f ↑t) ∨ ∃ (t : Finset (Fin n)), s < t.card ∧ StrictAntiOn f ↑t

docs, source

74. The Principle of Mathematical Induction #

Author: Leonardo de Moura

inductive Nat :
Type

docs, source

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)) :
∃ c ∈ Set.Ioo a b, deriv f c = (f b - f a) / (b - a)

docs, source

76. Fourier Series #

Author: Heather Macbeth

def fourierCoeff {T : ℝ} [hT : Fact (0 < T)] {E : Type} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : AddCircle T → E) (n : ℤ) :
E

docs, source

theorem hasSum_fourier_series_L2 {T : ℝ} [hT : Fact (0 < T)] (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) :
HasSum (fun (i : ℤ) => fourierCoeff (↑↑f) i • fourierLp 2 i) f

docs, source

77. Sum of kth powers #

Authors: Moritz Firsching and Fabian Kruse and Ashvni Narayanan

theorem sum_range_pow (n p : ℕ) :
∑ k ∈ Finset.range n, ↑k ^ p = ∑ i ∈ Finset.range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)

docs, source

theorem sum_Ico_pow (n p : ℕ) :
∑ k ∈ Finset.Ico 1 (n + 1), ↑k ^ p = ∑ i ∈ Finset.range (p + 1), bernoulli' i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)

docs, source

78. The Cauchy-Schwarz Inequality #

Author: Zhouhang Zhou

theorem inner_mul_inner_self_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :
‖inner x y‖ * ‖inner y x‖ ≤ RCLike.re (inner x x) * RCLike.re (inner y y)

docs, source

theorem norm_inner_le_norm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :
‖inner x y‖ ≤ ‖x‖ * ‖y‖

docs, source

79. The Intermediate Value Theorem #

Authors: Rob Lewis and Chris Hughes

theorem intermediate_value_Icc {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Set.Icc a b)) :
Set.Icc (f a) (f b) ⊆ f '' Set.Icc a b

docs, source

80. The Fundamental Theorem of Arithmetic #

Author: Chris Hughes

theorem Nat.primeFactorsList_unique {n : ℕ} {l : List ℕ} (h₁ : l.prod = n) (h₂ : ∀ p ∈ l, Nat.Prime p) :
l.Perm n.primeFactorsList

docs, source

instance Int.euclideanDomain :
EuclideanDomain ℤ

docs, source

instance EuclideanDomain.to_principal_ideal_domain {R : Type u} [EuclideanDomain R] :
IsPrincipalIdealRing R

docs, source

class UniqueFactorizationMonoid (α : Type u_2) [CancelCommMonoidWithZero α] extends IsWellFounded α DvdNotUnit :
Prop

docs, source

theorem UniqueFactorizationMonoid.factors_unique {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {f g : Multiset α} (hf : ∀ x ∈ f, Irreducible x) (hg : ∀ x ∈ g, Irreducible x) (h : Associated f.prod g.prod) :
Multiset.Rel Associated f g

docs, source

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 #

Author: Manuel Candales (archive), Michael Stoll (mathlib)

theorem Theorems100.Real.tendsto_sum_one_div_prime_atTop :
Filter.Tendsto (fun (n : ℕ) => ∑ p ∈ Finset.filter (fun (p : ℕ) => Nat.Prime p) (Finset.range n), 1 / ↑p) Filter.atTop Filter.atTop

docs, source

theorem not_summable_one_div_on_primes :
¬Summable ({p : ℕ | Nat.Prime p}.indicator fun (n : ℕ) => 1 / ↑n)

docs, source

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 : Set (Theorems100.«82».Cube n)}, s.Finite → s.Nontrivial → s.PairwiseDisjoint Theorems100.«82».Cube.toSet → ⋃ c ∈ s, c.toSet = Theorems100.«82».Cube.unitCube.toSet → Set.InjOn Theorems100.«82».Cube.w s → False

docs, source

83. The Friendship Theorem #

Authors: Aaron Anderson and Jalex Stark and Kyle Miller

theorem Theorems100.friendship_theorem {V : Type u} [Fintype V] {G : SimpleGraph V} (hG : Theorems100.Friendship G) [Nonempty V] :
Theorems100.ExistsPolitician G

docs, source

85. Divisibility by 3 Rule #

Author: Kim Morrison

theorem Nat.three_dvd_iff (n : ℕ) :
3 ∣ n ↔ 3 ∣ (Nat.digits 10 n).sum

docs, source

86. Lebesgue Measure and Integration #

Author: Johannes Hölzl

def MeasureTheory.lintegral {α : Type u_5} {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal) :
ENNReal

docs, source

88. Derangements Formula #

Author: Henry Swanson

theorem card_derangements_eq_numDerangements (α : Type u_2) [Fintype α] [DecidableEq α] :
Fintype.card ↑(derangements α) = numDerangements (Fintype.card α)

docs, source

theorem numDerangements_sum (n : ℕ) :
↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))

docs, source

89. The Factor and Remainder Theorems #

Author: Chris Hughes

theorem Polynomial.dvd_iff_isRoot {R : Type u} {a : R} [CommRing R] {p : Polynomial R} :
Polynomial.X - Polynomial.C a ∣ p ↔ p.IsRoot a

docs, source

theorem Polynomial.mod_X_sub_C_eq_C_eval {R : Type u} [Field R] (p : Polynomial R) (a : R) :
p % (Polynomial.X - Polynomial.C a) = Polynomial.C (Polynomial.eval a p)

docs, source

90. Stirling’s Formula #

Authors: Moritz Firsching and Fabian Kruse and Nikolas Kuhn and Heather Macbeth

theorem Stirling.tendsto_stirlingSeq_sqrt_pi :
Filter.Tendsto Stirling.stirlingSeq Filter.atTop (nhds √Real.pi)

docs, source

91. The Triangle Inequality #

Author: Zhouhang Zhou

theorem norm_add_le {E : Type u_5} [SeminormedAddGroup E] (a b : E) :
‖a + b‖ ≤ ‖a‖ + ‖b‖

docs, source

93. The Birthday Problem #

Author: Eric Rodriguez

theorem Theorems100.birthday :
2 * Fintype.card (Fin 23 ↪ Fin 365) < Fintype.card (Fin 23 → Fin 365) ∧ 2 * Fintype.card (Fin 22 ↪ Fin 365) > Fintype.card (Fin 22 → Fin 365)

docs, source

theorem Theorems100.birthday_measure :
MeasureTheory.volume {f : Fin 23 → Fin 365 | Function.Injective f} < 1 / 2

docs, source

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p1 p2 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 * Real.cos (EuclideanGeometry.angle p1 p2 p3)

docs, source

95. Ptolemy’s Theorem #

Author: Manuel Candales

theorem EuclideanGeometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {P : Type u_2} [MetricSpace P] [NormedAddTorsor V P] {a b c d p : P} (h : EuclideanGeometry.Cospherical {a, b, c, d}) (hapc : EuclideanGeometry.angle a p c = Real.pi) (hbpd : EuclideanGeometry.angle b p d = Real.pi) :
dist a b * dist c d + dist b c * dist d a = dist a c * dist b d

docs, source

96. Principle of Inclusion/Exclusion #

Author: Neil Strickland (outside mathlib), Yaël Dillies (in mathlib)

theorem Finset.inclusion_exclusion_sum_biUnion {ι : Type u_1} {α : Type u_2} {G : Type u_3} [DecidableEq α] [AddCommGroup G] (s : Finset ι) (S : ι → Finset α) (f : α → G) :
∑ a ∈ s.biUnion S, f a = ∑ t : { x : Finset ι // x ∈ Finset.filter (fun (x : Finset ι) => x.Nonempty) s.powerset }, (-1) ^ ((↑t).card + 1) • ∑ a ∈ (↑t).inf' ⋯ S, f a

docs, source

theorem Finset.inclusion_exclusion_card_biUnion {ι : Type u_1} {α : Type u_2} [DecidableEq α] (s : Finset ι) (S : ι → Finset α) :
↑(s.biUnion S).card = ∑ t : { x : Finset ι // x ∈ Finset.filter (fun (x : Finset ι) => x.Nonempty) s.powerset }, (-1) ^ ((↑t).card + 1) * ↑((↑t).inf' ⋯ S).card

docs, source

theorem Finset.inclusion_exclusion_sum_inf_compl {ι : Type u_1} {α : Type u_2} {G : Type u_3} [DecidableEq α] [AddCommGroup G] [Fintype α] (s : Finset ι) (S : ι → Finset α) (f : α → G) :
∑ a ∈ s.inf fun (i : ι) => (S i)ᶜ, f a = ∑ t ∈ s.powerset, (-1) ^ t.card • ∑ a ∈ t.inf S, f a

docs, source

theorem Finset.inclusion_exclusion_card_inf_compl {ι : Type u_1} {α : Type u_2} [DecidableEq α] [Fintype α] (s : Finset ι) (S : ι → Finset α) :
↑(s.inf fun (i : ι) => (S i)ᶜ).card = ∑ t ∈ s.powerset, (-1) ^ t.card * ↑(t.inf S).card

docs, source

github

97. Cramer’s Rule #

Author: Anne Baanen

theorem Matrix.mulVec_cramer {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (b : n → α) :
A.mulVec (A.cramer b) = A.det • b

docs, source

98. Bertrand’s Postulate #

Authors: Bolton Bailey and Patrick Stevens

theorem Nat.bertrand (n : ℕ) (hn0 : n ≠ 0) :
∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p ≤ 2 * n

docs, source

99. Buffon Needle Problem #

Author: Enrico Z. Borba

theorem BuffonsNeedle.buffon_short {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (d l : ℝ) (hd : 0 < d) (hl : 0 < l) (B : Ω → ℝ × ℝ) (hBₘ : Measurable B) (hB : MeasureTheory.pdf.IsUniform B (Set.Icc (-d / 2) (d / 2) ×ˢ Set.Icc 0 Real.pi) MeasureTheory.volume MeasureTheory.volume) (h : l ≤ d) :
∫ (x : Ω), BuffonsNeedle.N l B x = 2 * l * (d * Real.pi)⁻¹

docs, source

theorem BuffonsNeedle.buffon_long {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (d l : ℝ) (hd : 0 < d) (hl : 0 < l) (B : Ω → ℝ × ℝ) (hBₘ : Measurable B) (hB : MeasureTheory.pdf.IsUniform B (Set.Icc (-d / 2) (d / 2) ×ˢ Set.Icc 0 Real.pi) MeasureTheory.volume MeasureTheory.volume) (h : d ≤ l) :
∫ (x : Ω), BuffonsNeedle.N l B x = 2 * l / (d * Real.pi) - 2 / (d * Real.pi) * (√(l ^ 2 - d ^ 2) + d * Real.arcsin (d / l)) + 1

docs, source

100. Descartes Rule of Signs #

Author: Alex Meiburg

github