From 148c18bb25ceafbf9b75b5b3db5266f6de21fe53 Mon Sep 17 00:00:00 2001
From: leanprover-community-bot In 1. The Irrationality of the Square Root
+
@@ -77,7 +77,7 @@ 2. Fundamental Theorem of Algebra
(hf : 0 < f.degree)
:
3. The Denumerability of the Rational N
+
@@ -117,7 +117,7 @@ 4. Pythagorean Theorem
(p3 : P)
:
7. Law of Quadratic Reciprocity
(hpq : p ≠ q)
:
9. The Area of a Circle Theorems100.area_disc
(r : NNReal)
:
+
@@ -191,7 +191,7 @@ 10. Euler’s Generalization of Fermat
(h : x.Coprime n)
:
-
+
@@ -204,7 +204,7 @@ 11. The Infinitude of Primes Nat.exists_infinite_primes
(n : ℕ)
:
-
+
@@ -215,7 +215,7 @@ 14. Euler’s Summation of 1 + (1/2)^2
-
+
@@ -248,7 +248,7 @@ 15. Fundamental Theorem of Integral Ca
(hb : Filter.Tendsto f (nhds b ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c))
:
+
15. Fundamental Theorem of Integral Ca
(f'int : IntervalIntegrable f' MeasureTheory.volume a b)
:
16. Insolvability of General Higher De
+
@@ -302,7 +302,7 @@ 17. De Moivre’s Formula
(z : ℂ)
:
18. Liouville’s Theorem and the Cons
(lx : Liouville x)
:
-
+
@@ -330,7 +330,7 @@ 19. Four Squares Theorem Nat.sum_four_squares
(n : ℕ)
:
-
+
@@ -347,7 +347,7 @@ 20. All Primes (1 mod 4) Equal the Sum
(hp : p % 4 ≠ 3)
:
-
+
@@ -358,7 +358,7 @@ 22. The Non-Denumerability of the Cont
+
@@ -376,7 +376,7 @@ 23. Formula for Pythagorean Triples {z : ℤ}
:
-
+
@@ -406,7 +406,7 @@ 25. Schroeder-Bernstein Theorem
(hg : Function.Injective g)
:
26. Leibniz’s Series for Pi
27. Sum of the Angles of a Triangle
(h3 : p3 ≠ p1)
:
30. The Ballot Problem
(p : ℕ)
:
34. Divergence of the Harmonic Series
+
@@ -509,7 +509,7 @@ 35. Taylor’s Theorem (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x))
:
37. The Solution of a Cubic
(x : K)
:
38. Arithmetic Mean/Geometric Mean
(hz : ∀ i ∈ s, 0 ≤ z i)
:
-
+
@@ -638,7 +638,7 @@
39. Solutions to Pell’s Equation
(hp : x * x - Pell.d a1 * y * y = 1)
:
-
+
pell.eq_pell
, d
is defined to be a*a - 1
for an arbitrary a > 1
.
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.
@@ -1510,11 +1510,11 @@