Theorems 79 to 100

TheoremThe Fundamental Theorem of Arithmetic#

Mathlib records this with 5 declarations.

Nat.primeFactorsList_unique: Fundamental theorem of arithmetic

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

Int.euclideanDomain.

Int.euclideanDomain : EuclideanDomain ℤ

EuclideanDomain.instIsPrincipalIdealRing.

EuclideanDomain.instIsPrincipalIdealRing.{u} {R : Type u} [EuclideanDomain R] :
  IsPrincipalIdealRing R

UniqueFactorizationMonoid: Unique factorization monoids are defined as cancellative CommMonoidWithZeros with well-founded strict divisibility relations, but this is equivalent to more familiar definitions:

Each element (except zero) is uniquely represented as a multiset of irreducible factors. Uniqueness is only up to associated elements.

Each element (except zero) is non-uniquely represented as a multiset of prime factors.

To define a UFD using the definition in terms of multisets of irreducible factors, use the definition of_existsUnique_irreducible_factors

To define a UFD using the definition in terms of multisets of prime factors, use the definition of_exists_prime_factors

UniqueFactorizationMonoid.{u_2} (α : Type u_2) [CommMonoidWithZero α] : Prop

UniqueFactorizationMonoid.factors_unique.

UniqueFactorizationMonoid.factors_unique.{u_1} {α : Type u_1} [CommMonoidWithZero α]
  [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

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.

The 1000+ list (Q670235): 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.

Sources
MathlibNat.primeFactorsList_unique · Int.euclideanDomain · EuclideanDomain.instIsPrincipalIdealRing · UniqueFactorizationMonoid · UniqueFactorizationMonoid.factors_unique
Uses 6 · Used by 7
Statement usesEuclidean domain · Multiset · Principal ideal domain · Ring structure \(\Z\) · Unique factorisation domain
Proof usesCharacteristic zero
Used byInsolvability of General Higher Degree Equations (Abel-Ruffini Theorem) · Structure of finitely generated abelian groups · Structure theorem · Mason–Stothers theorem · Niven's theorem · Ostrowski's theorem · Jordan-Chevalley-Dunford decomposition

TheoremDivergence of the Prime Reciprocal Series#

Mathlib records this with 2 declarations.

Theorems100.Real.tendsto_sum_one_div_prime_atTop.

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

not_summable_one_div_on_primes: The sum over the reciprocals of the primes diverges.

not_summable_one_div_on_primes : ¬Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
Sources
MathlibTheorems100.Real.tendsto_sum_one_div_prime_atTop · not_summable_one_div_on_primes
Uses 12 · Used by 1
Statement usesBornology · Infinite sum · Irreducible element · Order
Proof usesCharacteristic zero · Completeness of R · Continuous function · Metric space · Order topology · The Infinitude of Primes · The Number of Subsets of a Set · Uniformly continuous function
Used byDirichlet’s Theorem

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

Dissection of Cubes: A cube cannot be cubed.

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
Sources
MathlibTheorems100.«82».cannot_cube_a_cube
Uses 3
Statement usesReal number
Proof usesCharacteristic zero · Order

TheoremThe Friendship Theorem#

Friendship theorem: We wish to show that a friendship graph has a politician (a vertex adjacent to all others). We proceed by contradiction, and assume the graph has no politician. We have already proven that a friendship graph with no politician is d-regular for some d, and now we do casework on d. If the degree is at most 2, we observe by casework that it has a politician anyway. If the degree is at least 3, the graph cannot exist.

Theorems100.friendship_theorem.{u} {V : Type u} [Fintype V] {G : SimpleGraph V}
  (hG : Theorems100.Friendship G) [Nonempty V] : Theorems100.ExistsPolitician G
Sources
MathlibTheorems100.friendship_theorem
Uses 10
Statement usesFinite set · Natural number · Simple graph
Proof usesAdjacency matrix · Characteristic zero · Field · Irreducible element · Ordered ring · Rational number · Ring structure \(\Z\)

TheoremDivisibility by 3 Rule#

Divisibility by 3 Rule

Nat.three_dvd_iff (n : ℕ) : 3 ∣ n ↔ 3 ∣ (Nat.digits 10 n).sum
Sources
MathlibNat.three_dvd_iff
Uses 2
Statement usesList · Natural number

TheoremDerangements Formula#

Mathlib records this with 2 declarations.

card_derangements_eq_numDerangements.

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

numDerangements_sum.

numDerangements_sum (n : ℕ) :
  ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
Sources
Mathlibcard_derangements_eq_numDerangements · numDerangements_sum
Uses 6
Statement usesFinite set · Integer · Permutation group of a type
Proof usesFixed points · Group morphism · Ring structure \(\Z\)

TheoremThe Factor and Remainder Theorems#

Mathlib records this with 2 declarations.

Polynomial.dvd_iff_isRoot.

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

Polynomial.mod_X_sub_C_eq_C_eval.

Polynomial.mod_X_sub_C_eq_C_eval.{u} {R : Type u} [Field R] (p : Polynomial R) (a : R) :
  p % (Polynomial.X - Polynomial.C a) = Polynomial.C (Polynomial.eval a p)
Sources
MathlibPolynomial.dvd_iff_isRoot · Polynomial.mod_X_sub_C_eq_C_eval
Uses 5 · Used by 2
Statement usesField · Linear map · Polynomial functions · Rational number
Proof usesCharacteristic zero
Used byMultiplicity · Roots of a polynomial

TheoremStirling’s Formula#

Stirling's Formula

Stirling.tendsto_stirlingSeq_sqrt_pi :
  Filter.Tendsto Stirling.stirlingSeq Filter.atTop (nhds √Real.pi)
Sources
MathlibStirling.tendsto_stirlingSeq_sqrt_pi
Uses 15
Statement usesBornology · Cos (extension of trigonometric functions to the complex plane) · Exponential
Proof usesAssociative algebra over a commutative ring · Characteristic p · Characteristic zero · Completeness of R · Derivative of the inverse of a function (Single Variable Real Analysis) · Field \(\Q\) of rational numbers · Hausdorff space · Infinite sum · Logarithm · Metric structure · Order topology · The Binomial Theorem

TheoremThe Triangle Inequality#

Triangle inequality for the norm.

norm_add_le.{u_4} {E : Type u_4} [SeminormedAddGroup E] (a b : E) : ‖a + b‖ ≤ ‖a‖ + ‖b‖
Sources
Mathlibnorm_add_le
Uses 2 · Used by 24
Statement usesBornology · Order
Used byBuffon Needle Problem · Maximum modulus principle · Change of variables formula · Absolutely convergent series in Banach spaces · Banach-Steinhaus theorem · Hahn-Banach theorem · Jacobi/Leibniz identity · Closed interval · Strong law of large numbers · Stone-Weierstrass theorem · Urysohn's lemma · Gershgorin circle theorem · Abel's theorem · Rademacher's theorem · Fernique's theorem · Borel–Carathéodory theorem · Morera's theorem · Fourier theorem · Gelfand–Mazur theorem · Akra–Bazzi theorem · Poisson limit theorem · Partial derivatives commute · Continuity (continuity and differentiability of convex functions) · Differentiability of the limit of a sequence of functions

TheoremThe Birthday Problem#

Mathlib records this with 2 declarations.

Theorems100.birthday: Birthday Problem: set cardinality interpretation.

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)

Theorems100.birthday_measure: Birthday Problem: first probabilistic interpretation.

Theorems100.birthday_measure : MeasureTheory.volume {f | Function.Injective f} < 1 / 2
Sources
MathlibTheorems100.birthday · Theorems100.birthday_measure
Uses 6
Statement usesLebesgue measure (Measure theory)
Proof usesCharacteristic zero · Conditional probability · Counting measure · Ordered ring · Product of sigma-algebras

TheoremThe Law of Cosines#

Law of cosines (cosine rule), angle-at-point form.

EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle.{u_1, u_2}
  {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
  [NormedAddTorsor V P] (p₁ p₂ p₃ : P) :
  dist p₁ p₃ * dist p₁ p₃ =
    dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ -
      2 * dist p₁ p₂ * dist p₃ p₂ * Real.cos (EuclideanGeometry.angle p₁ p₂ p₃)
Sources
MathlibEuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle
Uses 2 · Used by 2
Statement usesAngle · Euclidean affine space
Used byHeron’s Formula · Stewart's theorem

TheoremPtolemy’s Theorem#

Ptolemy’s Theorem.

EuclideanGeometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical.{u_1, u_2} {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
Sources
MathlibEuclideanGeometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical
Uses 4
Statement usesAngle · Euclidean affine space
Proof usesProduct of Segments of Chords · Stewart's theorem

TheoremPrinciple of Inclusion/Exclusion#

Mathlib records this with 4 declarations.

Finset.inclusion_exclusion_sum_biUnion: Inclusion-exclusion principle for the sum of a function over a union.

The sum of a function f over the union of the S i over i ∈ s is the alternating sum of the sums of f over the intersections of the S i.

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

Finset.inclusion_exclusion_card_biUnion: Inclusion-exclusion principle for the cardinality of a union.

The cardinality of the union of the S i over i ∈ s is the alternating sum of the cardinalities of the intersections of the S i.

Finset.inclusion_exclusion_card_biUnion.{u_1, u_2} {ι : Type u_1} {α : Type u_2} [DecidableEq α]
  (s : Finset ι) (S : ι → Finset α) :
  ↑(s.biUnion S).card = ∑ t, (-1) ^ ((↑t).card + 1) * ↑((↑t).inf' ⋯ S).card

Finset.inclusion_exclusion_sum_inf_compl: Inclusion-exclusion principle for the sum of a function over an intersection of complements.

The sum of a function f over the intersection of the complements of the S i over i ∈ s is the alternating sum of the sums of f over the intersections of the S i.

Finset.inclusion_exclusion_sum_inf_compl.{u_1, u_2, u_3} {ι : Type u_1} {α : Type u_2}
  {G : Type u_3} [AddCommGroup G] [DecidableEq α] [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

Finset.inclusion_exclusion_card_inf_compl: Inclusion-exclusion principle for the cardinality of an intersection of complements.

The cardinality of the intersection of the complements of the S i over i ∈ s is the alternating sum of the cardinalities of the intersections of the S i.

Finset.inclusion_exclusion_card_inf_compl.{u_1, u_2} {ι : 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
Sources
MathlibFinset.inclusion_exclusion_sum_biUnion · Finset.inclusion_exclusion_card_biUnion · Finset.inclusion_exclusion_sum_inf_compl · Finset.inclusion_exclusion_card_inf_compl
Uses 4
Statement usesFinite set · Integer
Proof usesModule · Ring structure \(\Z\)

TheoremCramer’s Rule#

A stronger form of Cramer's rule that allows us to solve some instances of A * x = b even if the determinant is not a unit. A sufficient (but still not necessary) condition is that A.det divides b.

Matrix.mulVec_cramer.{v, w} {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α]
  (A : Matrix n n α) (b : n → α) : A.mulVec (A.cramer b) = A.det • b
Sources
MathlibMatrix.mulVec_cramer
Uses 1
Statement usesDeterminant

TheoremBertrand’s Postulate#

Alias of Nat.exists_prime_lt_and_le_two_mul.

Bertrand's Postulate: For any positive natural number, there is a prime which is greater than it, but no more than twice as large.

Nat.bertrand (n : ℕ) (hn0 : n ≠ 0) : ∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
Sources
MathlibNat.bertrand
Uses 9
Statement usesIrreducible element · Natural number
Proof usesAssociative algebra over a commutative ring · Characteristic zero · Convex function · Finitely supported function · Linear map · Logarithm · Ordered ring

TheoremBuffon Needle Problem#

Mathlib records this with 2 declarations.

BuffonsNeedle.buffon_short: Buffon's Needle, the short case (l ≤ d). The probability of the needle crossing a line equals (2 * l) / (d * π).

BuffonsNeedle.buffon_short.{u_1} {Ω : 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)⁻¹

BuffonsNeedle.buffon_long: Buffon's Needle, the long case (d ≤ l)

BuffonsNeedle.buffon_long.{u_1} {Ω : 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
Sources
MathlibBuffonsNeedle.buffon_short · BuffonsNeedle.buffon_long
Uses 11
Statement usesBochner integral · Conditional probability · Inverse trigonometric functions · Lebesgue measure (Measures and integral calculus) · Measurable function
Proof usesCharacteristic zero · Compactness in terms of filters · Euclidean domain · Fubini's theorem · The Triangle Inequality · Topological ring

TheoremDescartes Rule of Signs#

Descartes' Rule of Signs: the number of positive roots is at most the number of sign variations.

Polynomial.roots_countP_pos_le_signVariations.{u_1} {R : Type u_1} [CommRing R] [LinearOrder R]
  [IsStrictOrderedRing R] (P : Polynomial R) :
  Multiset.countP (fun x => 0 < x) P.roots ≤ P.signVariations
Sources
MathlibPolynomial.roots_countP_pos_le_signVariations
Uses 2
Statement usesRoots of a polynomial
Proof usesOrdered ring

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.