This webpage is about Lean 3, which is effectively obsolete; the community has migrated to Lean 4.

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

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.is_root z

docs, source

3. The Denumerability of the Rational Numbers #

Author: Chris Hughes

def rat.denumerable  :
denumerable ℚ

docs, source

4. Pythagorean Theorem #

Author: Joseph Myers

theorem euclidean_geometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (p1 p2 p3 : P) :
has_dist.dist p1 p3 * has_dist.dist p1 p3 = has_dist.dist p1 p2 * has_dist.dist p1 p2 + has_dist.dist p3 p2 * has_dist.dist p3 p2 ↔ euclidean_geometry.angle p1 p2 p3 = real.pi / 2

docs, source

7. Law of Quadratic Reciprocity #

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

theorem legendre_sym.quadratic_reciprocity {p q : ℕ} [fact (nat.prime p)] [fact (nat.prime q)] (hp : p ≠ 2) (hq : q ≠ 2) (hpq : p ≠ q) :
legendre_sym q ↑p * legendre_sym p ↑q = (-1) ^ (p / 2 * (q / 2))

docs, source

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

docs, source

9. The Area of a Circle #

Authors: James Arthur, Benjamin Davidson, and Andrew Souther

mathlib archive

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, David Loeffler

theorem has_sum_zeta_two  :
has_sum (λ (n : ℕ), 1 / ↑n ^ 2) (real.pi ^ 2 / 6)

docs, source

15. Fundamental Theorem of Integral Calculus #

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

theorem interval_integral.integral_has_strict_deriv_at_of_tendsto_ae_right {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) (hmeas : strongly_measurable_at_filter f (nhds b) measure_theory.measure_space.volume) (hb : filter.tendsto f (nhds b ⊓ measure_theory.measure_space.volume.ae) (nhds c)) :
has_strict_deriv_at (λ (u : ℝ), ∫ (x : ℝ) in a..u, f x) c b

docs, source

theorem interval_integral.integral_eq_sub_of_has_deriv_right_of_le {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E} (hab : a ≤ b) (hcont : continuous_on f (set.Icc a b)) (hderiv : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_within_at f (f' x) (set.Ioi x) x) (f'int : interval_integrable f' measure_theory.measure_space.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

mathlib archive

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 pythagorean_triple.classification {x y z : ℤ} :
pythagorean_triple 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 #

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 : 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 (λ (k : ℕ), (finset.range k).sum (λ (i : ℕ), (-1) ^ i / (2 * ↑i + 1))) filter.at_top (nhds (real.pi / 4))

docs, source

27. Sum of the Angles of a Triangle #

Author: Joseph Myers

theorem euclidean_geometry.angle_add_angle_add_angle_eq_pi {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {p1 p2 p3 : P} (h2 : p2 ≠ p1) (h3 : p3 ≠ p1) :
euclidean_geometry.angle p1 p2 p3 + euclidean_geometry.angle p2 p3 p1 + euclidean_geometry.angle p3 p1 p2 = real.pi

docs, source

30. The Ballot Problem #

Authors: Bhavik Mehta, Kexing Ying

mathlib archive

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_at_top  :
filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), 1 / (↑i + 1))) filter.at_top filter.at_top

docs, source

35. Taylor’s Theorem #

Author: Moritz Doll

theorem taylor_mean_remainder_lagrange {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ} (hx : x₀ < x) (hf : cont_diff_on ℝ ↑n f (set.Icc x₀ x)) (hf' : differentiable_on ℝ (iterated_deriv_within n f (set.Icc x₀ x)) (set.Ioo x₀ x)) :
∃ (x' : ℝ) (hx' : x' ∈ set.Ioo x₀ x), f x - taylor_within_eval f n (set.Icc x₀ x) x₀ x = iterated_deriv_within (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 : cont_diff_on ℝ ↑n f (set.Icc x₀ x)) (hf' : differentiable_on ℝ (iterated_deriv_within n f (set.Icc x₀ x)) (set.Ioo x₀ x)) :
∃ (x' : ℝ) (hx' : x' ∈ set.Ioo x₀ x), f x - taylor_within_eval f n (set.Icc x₀ x) x₀ x = iterated_deriv_within (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

mathlib archive

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 : ι), i ∈ s → 0 ≤ w i) (hw' : s.sum (λ (i : ι), w i) = 1) (hz : ∀ (i : ι), i ∈ s → 0 ≤ z i) :
s.prod (λ (i : ι), z i ^ w i) ≤ s.sum (λ (i : ι), w i * z i)

docs, source

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 - d a1 * y * y = 1) :
∃ (n : ℕ), x = pell.xn a1 n ∧ y = pell.yn a1 n

docs, source

theorem pell.exists_of_not_is_square {d : ℤ} (h₀ : 0 < d) (hd : ¬is_square 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, Yaël Dillies

theorem measure_theory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure {E : Type u_1} [measurable_space E] {μ : measure_theory.measure E} {F s : set E} [normed_add_comm_group E] [normed_space ℝ E] [borel_space E] [finite_dimensional ℝ E] [μ.is_add_haar_measure] {L : add_subgroup E} [countable ↥L] (fund : measure_theory.is_add_fundamental_domain ↥L F μ) (h : ⇑μ F * 2 ^ fdim E < ⇑μ s) (h_symm : ∀ (x : E), x ∈ s → -x ∈ s) (h_conv : convex ℝ s) :
∃ (x : ↥L) (H : x ≠ 0), ↑x ∈ s

docs, source

42. Sum of the Reciprocals of the Triangular Numbers #

Authors: Jalex Stark, Yury Kudryashov

mathlib archive

44. The Binomial Theorem #

Author: Chris Hughes

theorem add_pow {R : Type u_1} [comm_semiring R] (x y : R) (n : ℕ) :
(x + y) ^ n = (finset.range (n + 1)).sum (λ (m : ℕ), x ^ m * y ^ (n - m) * ↑(n.choose m))

docs, source

45. The Partition Theorem #

Authors: Bhavik Mehta, Aaron Anderson

mathlib archive

49. The Cayley-Hamilton Theorem #

Author: Scott Morrison

theorem matrix.aeval_self_charpoly {R : Type u} [comm_ring R] {n : Type w} [decidable_eq 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

mathlib archive

55. Product of Segments of Chords #

Author: Manuel Candales

theorem euclidean_geometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] {P : Type u_2} [metric_space P] [normed_add_torsor V P] {a b c d p : P} (h : euclidean_geometry.cospherical {a, b, c, d}) (hapb : euclidean_geometry.angle a p b = real.pi) (hcpd : euclidean_geometry.angle c p d = real.pi) :
has_dist.dist a p * has_dist.dist b p = has_dist.dist c p * has_dist.dist d p

docs, source

57. Heron’s Formula #

Author: Matt Kempster

mathlib archive

58. Formula for the Number of Combinations #

Author: mathlib

theorem finset.card_powerset_len {α : Type u_1} (n : ℕ) (s : finset α) :
(finset.powerset_len n s).card = s.card.choose n

docs, source

theorem finset.mem_powerset_len {α : Type u_1} {n : ℕ} {s t : finset α} :
s ∈ finset.powerset_len n t ↔ s ⊆ t ∧ s.card = n

docs, source

59. The Laws of Large Numbers #

Author: Sébastien Gouëzel

theorem probability_theory.strong_law_ae {Ω : Type u_1} [measure_theory.measure_space Ω] [measure_theory.is_probability_measure measure_theory.measure_space.volume] (X : ℕ → Ω → ℝ) (hint : measure_theory.integrable (X 0) measure_theory.measure_space.volume) (hindep : pairwise (λ (i j : ℕ), probability_theory.indep_fun (X i) (X j) measure_theory.measure_space.volume)) (hident : ∀ (i : ℕ), probability_theory.ident_distrib (X i) (X 0) measure_theory.measure_space.volume measure_theory.measure_space.volume) :
∀ᵐ (ω : Ω), filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), X i ω) / ↑n) filter.at_top (nhds (∫ (a : Ω), X 0 a))

docs, source

60. Bezout’s Theorem #

Author: mathlib

theorem nat.gcd_eq_gcd_ab (x y : ℕ) :
↑(x.gcd y) = ↑x * x.gcd_a y + ↑y * x.gcd_b y

docs, source

62. Fair Games Theorem #

Author: Kexing Ying

theorem measure_theory.submartingale_iff_expected_stopped_value_mono {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {𝒢 : measure_theory.filtration ℕ m0} {f : ℕ → Ω → ℝ} [measure_theory.is_finite_measure μ] (hadp : measure_theory.adapted 𝒢 f) (hint : ∀ (i : ℕ), measure_theory.integrable (f i) μ) :
measure_theory.submartingale f 𝒢 μ ↔ ∀ (τ π : Ω → ℕ), measure_theory.is_stopping_time 𝒢 τ → measure_theory.is_stopping_time 𝒢 π → τ ≤ π → (∃ (N : ℕ), ∀ (x : Ω), π x ≤ N) → ∫ (x : Ω), measure_theory.stopped_value f τ x ∂μ ≤ ∫ (x : Ω), measure_theory.stopped_value f π x ∂μ

docs, source

63. Cantor’s Theorem #

Author: mathlib

theorem cardinal.cantor (a : cardinal) :
a < 2 ^ a

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, differentiable_at ℝ 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 (λ (x : ℝ), deriv f x / deriv g x) (nhds a) l) :
filter.tendsto (λ (x : ℝ), f x / g x) (nhds_within a {a}ᶜ) l

docs, source

65. Isosceles Triangle Theorem #

Author: Joseph Myers

theorem euclidean_geometry.angle_eq_angle_of_dist_eq {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {p1 p2 p3 : P} (h : has_dist.dist p1 p2 = has_dist.dist p1 p3) :
euclidean_geometry.angle p1 p2 p3 = euclidean_geometry.angle p1 p3 p2

docs, source

66. Sum of a Geometric Series #

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

theorem geom_sum_Ico {α : Type u} [division_ring α] {x : α} (hx : x ≠ 1) {m n : ℕ} (hmn : m ≤ n) :
(finset.Ico m n).sum (λ (i : ℕ), x ^ i) = (x ^ n - x ^ m) / (x - 1)

docs, source

theorem nnreal.has_sum_geometric {r : nnreal} (hr : r < 1) :
has_sum (λ (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 : ℕ) :
(finset.range n).sum (λ (i : ℕ), i) = n * (n - 1) / 2

docs, source

69. Greatest Common Divisor Algorithm #

Author: mathlib

def euclidean_domain.gcd {R : Type u} [euclidean_domain R] [decidable_eq R] :
R → R → R

docs, source

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

docs, source

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

docs, source

70. The Perfect Number Theorem #

Author: Aaron Anderson

mathlib archive

71. Order of a Subgroup #

Author: mathlib

theorem subgroup.card_subgroup_dvd_card {α : Type u_1} [group α] [fintype α] (s : subgroup α) [fintype ↥s] :
fintype.card ↥s ∣ fintype.card α

docs, source

72. Sylow’s Theorem #

Author: Chris Hughes

theorem sylow.exists_subgroup_card_pow_prime {G : Type u} [group G] [fintype G] (p : ℕ) {n : ℕ} [fact (nat.prime p)] (hdvd : p ^ n ∣ fintype.card G) :
∃ (K : subgroup G), fintype.card ↥K = p ^ n

docs, source

sylow_conjugate

card_sylow_dvd

card_sylow_modeq_one

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

Author: Bhavik Mehta

mathlib archive

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 : continuous_on f (set.Icc a b)) (hfd : differentiable_on ℝ f (set.Ioo a b)) :
∃ (c : ℝ) (H : c ∈ set.Ioo a b), deriv f c = (f b - f a) / (b - a)

docs, source

76. Fourier Series #

Author: Heather Macbeth

noncomputable def fourier_coeff {T : ℝ} [hT : fact (0 < T)] {E : Type} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] (f : add_circle T → E) (n : ℤ) :
E

docs, source

theorem has_sum_fourier_series_L2 {T : ℝ} [hT : fact (0 < T)] (f : ↥(measure_theory.Lp ℂ 2 add_circle.haar_add_circle)) :
has_sum (λ (i : ℤ), fourier_coeff ⇑f i • fourier_Lp 2 i) f

docs, source

77. Sum of kth powers #

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

theorem sum_range_pow (n p : ℕ) :
(finset.range n).sum (λ (k : ℕ), ↑k ^ p) = (finset.range (p + 1)).sum (λ (i : ℕ), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1))

docs, source

theorem sum_Ico_pow (n p : ℕ) :
(finset.Ico 1 (n + 1)).sum (λ (k : ℕ), ↑k ^ p) = (finset.range (p + 1)).sum (λ (i : ℕ), 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} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (x y : E) :
‖has_inner.inner x y‖ * ‖has_inner.inner y x‖ ≤ ⇑is_R_or_C.re (has_inner.inner x x) * ⇑is_R_or_C.re (has_inner.inner y y)

docs, source

theorem norm_inner_le_norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (x y : E) :
‖has_inner.inner x y‖ ≤ ‖x‖ * ‖y‖

docs, source

79. The Intermediate Value Theorem #

Author: mathlib (Rob Lewis and Chris Hughes)

theorem intermediate_value_Icc {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {a b : α} (hab : a ≤ b) {f : α → δ} (hf : continuous_on 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: mathlib (Chris Hughes)

theorem nat.factors_unique {n : ℕ} {l : list ℕ} (h₁ : l.prod = n) (h₂ : ∀ (p : ℕ), p ∈ l → nat.prime p) :
l ~ n.factors

docs, source

def int.euclidean_domain  :
euclidean_domain ℤ

docs, source

def euclidean_domain.to_principal_ideal_domain {R : Type u} [euclidean_domain R] :
is_principal_ideal_ring R

docs, source

structure unique_factorization_monoid (α : Type u_2) [cancel_comm_monoid_with_zero α] :
Prop

docs, source

theorem unique_factorization_monoid.factors_unique {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] {f g : multiset α} (hf : ∀ (x : α), x ∈ f → irreducible x) (hg : ∀ (x : α), 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

mathlib archive

82. Dissection of Cubes (J.E. Littlewood’s ‘elegant’ proof) #

Author: Floris van Doorn

mathlib archive

83. The Friendship Theorem #

Authors: Aaron Anderson, Jalex Stark, Kyle Miller

mathlib archive

85. Divisibility by 3 Rule #

Author: Scott Morrison

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

docs, source

86. Lebesgue Measure and Integration #

Author: Johannes Hölzl

noncomputable def measure_theory.lintegral {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) (f : α → ennreal) :
ennreal

docs, source

88. Derangements Formula #

Author: Henry Swanson

theorem card_derangements_eq_num_derangements (α : Type u_1) [fintype α] [decidable_eq α] :
fintype.card ↥(derangements α) = num_derangements (fintype.card α)

docs, source

theorem num_derangements_sum (n : ℕ) :
↑(num_derangements n) = (finset.range (n + 1)).sum (λ (k : ℕ), (-1) ^ k * ↑(k.asc_factorial (n - k)))

docs, source

89. The Factor and Remainder Theorems #

Author: Chris Hughes

theorem polynomial.dvd_iff_is_root {R : Type u} {a : R} [comm_ring R] {p : polynomial R} :
polynomial.X - ⇑polynomial.C a ∣ p ↔ p.is_root 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: mathlib (Moritz Firsching, Fabian Kruse, Nikolas Kuhn, Heather Macbeth)

theorem stirling.tendsto_stirling_seq_sqrt_pi  :
filter.tendsto (λ (n : ℕ), stirling.stirling_seq n) filter.at_top (nhds (√ real.pi))

docs, source

91. The Triangle Inequality #

Author: Zhouhang Zhou

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

docs, source

93. The Birthday Problem #

Author: Eric Rodriguez

mathlib archive

94. The Law of Cosines #

Author: Joseph Myers

theorem euclidean_geometry.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} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (p1 p2 p3 : P) :
has_dist.dist p1 p3 * has_dist.dist p1 p3 = has_dist.dist p1 p2 * has_dist.dist p1 p2 + has_dist.dist p3 p2 * has_dist.dist p3 p2 - 2 * has_dist.dist p1 p2 * has_dist.dist p3 p2 * real.cos (euclidean_geometry.angle p1 p2 p3)

docs, source

95. Ptolemy’s Theorem #

Author: Manuel Candales

theorem euclidean_geometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] {P : Type u_2} [metric_space P] [normed_add_torsor V P] {a b c d p : P} (h : euclidean_geometry.cospherical {a, b, c, d}) (hapc : euclidean_geometry.angle a p c = real.pi) (hbpd : euclidean_geometry.angle b p d = real.pi) :
has_dist.dist a b * has_dist.dist c d + has_dist.dist b c * has_dist.dist d a = has_dist.dist a c * has_dist.dist b d

docs, source

96. Principle of Inclusion/Exclusion #

Author: Neil Strickland

github

97. Cramer’s Rule #

Author: Anne Baanen

theorem matrix.mul_vec_cramer {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] (A : matrix n n α) (b : n → α) :
A.mul_vec (⇑(A.cramer) b) = A.det • b

docs, source

98. Bertrand’s Postulate #

Authors: Bolton Bailey, Patrick Stevens

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

docs, source