Theorems 1 to 27

TheoremThe Irrationality of the Square Root of 2#

Irrationality of the Square Root of 2

irrational_sqrt_two : Irrational √2
Sources
Mathlibirrational_sqrt_two
Uses 5
Statement usesOrder
Proof usesCharacteristic zero · Field \(\R\) of real numbers · Irreducible element · Ordered ring

InstanceThe Denumerability of the Rational Numbers#

Denumerability of the Rational Numbers

Rat.instDenumerable : Denumerable ℚ
Sources
MathlibRat.instDenumerable
Uses 2
Statement usesList · Rational number

TheoremPythagorean Theorem#

Pythagorean theorem, if-and-only-if angle-at-point form.

EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two.{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₂ ↔
    EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2
Sources
MathlibEuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two
Uses 2
Statement usesAngle · Euclidean affine space

TheoremThe Area of a Circle#

Area of a Circle: The area of a disc with radius r is π * r ^ 2.

Theorems100.area_disc (r : NNReal) :
  MeasureTheory.volume (Theorems100.disc ↑r) = ↑NNReal.pi * ↑r ^ 2
Sources
MathlibTheorems100.area_disc
Uses 9
Statement usesCos (extension of trigonometric functions to the complex plane) · Lebesgue measure (Measures and integral calculus)
Proof usesCharacteristic zero · Continuity of monotone functions · Derivative at a point · Fundamental theorem of calculus, part 2 · Giry monad · Hausdorff space · Inverse trigonometric functions

TheoremEuler’s Generalization of Fermat’s Little Theorem#

The Fermat-Euler totient theorem. ZMod.pow_totient is an alternative statement of the same theorem.

Nat.ModEq.pow_totient {x n : ℕ} (h : x.Coprime n) : x ^ n.totient ≡ 1 [MOD n]
Sources
MathlibNat.ModEq.pow_totient
Uses 2
Statement usesEuler's totient function (\(\varphi\))
Proof usesFinite set

TheoremThe Infinitude of Primes#

Euclid's theorem on the infinitude of primes. Here given in the form: for every n, there exists a prime number p ≥ n.

Nat.exists_infinite_primes (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p
Sources
MathlibNat.exists_infinite_primes
Uses 2 · Used by 1
Statement usesIrreducible element · Natural number
Used byDivergence of the Prime Reciprocal Series

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

Mathlib states this as hasSum_zeta_two.

hasSum_zeta_two : HasSum (fun n => 1 / ↑n ^ 2) (Real.pi ^ 2 / 6)
Sources
MathlibhasSum_zeta_two
Uses 12
Statement usesBornology · Cos (extension of trigonometric functions to the complex plane) · Infinite sum
Proof usesAbsolutely convergent series in Banach spaces · Bernoulli numbers · Characteristic p · Derivative at a point · Euclidean domain · Fourier Series · Fundamental theorem of calculus, part 2 · Polynomial derivative · Uniformly continuous function

TheoremFundamental Theorem of Integral Calculus#

Mathlib records this with 2 declarations.

intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_right: Fundamental theorem of calculus-1, strict differentiability in the right endpoint.

If f : ℝ → E is integrable on a..b and f x has a finite limit c almost surely at b, then u ↦ ∫ x in a..u, f x has derivative c at b in the sense of strict differentiability.

intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_right.{u_3} {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

intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le: Fundamental theorem of calculus-2: If f : ℝ → E is continuous on [a, b] (where a ≤ b) and has a right derivative at f' x for all x in (a, b), and f' is integrable on [a, b], then ∫ y in a..b, f' y equals f b - f a.

intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le.{u_3} {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
Sources
MathlibintervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_right · intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le
Uses 15 · Used by 2
Statement usesBochner integral · Carathéodory's theorem (measure theory) · Lebesgue measure (Measures and integral calculus) · Topological module
Proof usesAffine space · Compactness in terms of filters · Completeness of R · Differentiable function between normed vector spaces · Dual of a normed space · Extended real number · Local convexity · Measurable function · Metric structure · Order topology · Topological ring
Used byMorera's theorem · Antiderivative of a continuous function

TheoremInsolvability of General Higher Degree Equations (Abel-Ruffini Theorem)#

Abel-Ruffini Theorem

AbelRuffini.exists_not_solvable_by_rad : ∃ x, IsAlgebraic ℚ x ∧ x ∉ solvableByRad ℚ ℂ
Sources
MathlibAbelRuffini.exists_not_solvable_by_rad
Uses 11
Statement usesAlgebraic elements · Characteristic zero · Field \(\C\) of complex numbers · Field \(\Q\) of rational numbers
Proof usesAbel-Ruffini theorem (one direction) · Eisenstein's criterion · Fundamental theorem of algebra · Intermediate value theorem · Rolle's theorem · Separable polynomial · The Fundamental Theorem of Arithmetic

TheoremDe Moivre’s Formula#

De Moivre's formula

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
Sources
MathlibComplex.cos_add_sin_mul_I_pow
Uses 4
Statement usesCos (extension of trigonometric functions to the complex plane) · Sin (extension of trigonometric functions to the complex plane)
Proof usesCharacteristic zero · Field \(\C\) of complex numbers

TheoremLiouville’s Theorem and the Construction of Transcendental Numbers#

Liouville's Theorem

Liouville.transcendental {x : ℝ} (lx : Liouville x) : Transcendental ℤ x
Sources
MathlibLiouville.transcendental
Uses 15 · Used by 1
Statement usesReal number · Ring structure \(\Z\) · Transcendental elements
Proof usesClosure · Completeness · Convex subsets · Differentiable function between normed vector spaces · Differentials (linear tangent functions) · Extreme value theorem · Field \(\R\) of real numbers · Normed vector space over a normed field · Order topology · Ordered ring · Roots of a polynomial · Topological ring
Used byLiouville's theorem on existence of transcendental numbers

TheoremThe Non-Denumerability of the Continuum#

Mathlib states this as Cardinal.not_countable_real.

Cardinal.not_countable_real : ¬Set.univ.Countable
Sources
MathlibCardinal.not_countable_real
Uses 11
Statement usesReal number
Proof usesCardinal · Characteristic zero · Completeness of R · Field \(\Q\) of rational numbers · Hausdorff space · Infinite sum · Metric structure · Order topology · Topological ring · Uniformly continuous function

TheoremFormula for Pythagorean Triples#

Formula for Pythagorean Triples

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))
Sources
MathlibPythagoreanTriple.classification
Uses 8
Statement usesInteger
Proof uses\(\Z\) is a Euclidean ring · Characteristic p · Characteristic zero · Field \(\Q\) of rational numbers · Finite set · Irreducible element · Ordered ring

TheoremSchroeder-Bernstein Theorem#

The Schröder-Bernstein Theorem: Given injections α → β and β → α, we can get a bijection α → β.

Function.Embedding.schroeder_bernstein.{u, v} {α : Type u} {β : Type v} {f : α → β} {g : β → α}
  (hf : Function.Injective f) (hg : Function.Injective g) : ∃ h, Function.Bijective h
Sources
MathlibFunction.Embedding.schroeder_bernstein
Uses 1
Proof usesSet

TheoremLeibniz’s Series for Pi#

Leibniz's series for π. The alternating sum of odd number reciprocals is π / 4, proved by using Abel's limit theorem to extend the Maclaurin series of arctan to 1.

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))
Sources
MathlibReal.tendsto_sum_pi_div_four
Uses 5
Statement usesBornology · Cos (extension of trigonometric functions to the complex plane)
Proof usesAbel's theorem · Alternating series · Log

TheoremSum of the Angles of a Triangle#

The sum of the angles of a triangle (possibly degenerate, where two given vertices are distinct), angle-at-point.

EuclideanGeometry.angle_add_angle_add_angle_eq_pi.{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₃ : P) (h : p₂ ≠ p₁) :
  EuclideanGeometry.angle p₁ p₂ p₃ + EuclideanGeometry.angle p₂ p₃ p₁ +
      EuclideanGeometry.angle p₃ p₁ p₂ =
    Real.pi
Sources
MathlibEuclideanGeometry.angle_add_angle_add_angle_eq_pi
Uses 5 · Used by 1
Statement usesAngle · Euclidean affine space
Proof usesCauchy-Schwarz inequality · Characteristic zero · Ordered ring
Used byExterior angle theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.