From 674152da7a98acf3cc177438dd7180b10ca102ce Mon Sep 17 00:00:00 2001 From: leanprover-community-bot Date: Sat, 21 Oct 2023 22:00:21 +0000 Subject: [PATCH] deploy site from ea41003c269327007cbeb9f975c3ea2b4a844030 --- 100.html | 148 ++++++++++++++++++++-------------------- mathlib_stats.html | 4 +- teaching/practices.html | 3 +- 3 files changed, 77 insertions(+), 78 deletions(-) diff --git a/100.html b/100.html index b2f3675a61..27c8721904 100644 --- a/100.html +++ b/100.html @@ -62,7 +62,7 @@
1. The Irrationality of the Square Root
theorem irrational_sqrt_two :
Irrational (Real.sqrt 2)
-

docs, source

+

docs, source

@@ -77,7 +77,7 @@
2. Fundamental Theorem of Algebra (hf : 0 < Polynomial.degree f) :
∃ z, Polynomial.IsRoot f z
-

docs, source

+

docs, source

@@ -88,7 +88,7 @@
3. The Denumerability of the Rational N
instance Rat.instDenumerableRat :
Denumerable ℚ
-

docs, source

+

docs, source

@@ -117,7 +117,7 @@
4. Pythagorean Theorem (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

+

docs, source

@@ -142,7 +142,7 @@
7. Law of Quadratic Reciprocity (hpq : p ≠ q) :
legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
-

docs, source

+

docs, source

theorem jacobiSym.quadratic_reciprocity @@ -154,7 +154,7 @@
7. Law of Quadratic Reciprocity (hb : Odd b) :
jacobiSym (↑a) b = (-1) ^ (a / 2 * (b / 2)) * jacobiSym (↑b) a
-

docs, source

+

docs, source

@@ -178,7 +178,7 @@
10. Euler’s Generalization of Fermat (h : Nat.Coprime x n) :
x ^ Nat.totient n ≡ 1 [MOD n]
-

docs, source

+

docs, source

@@ -191,7 +191,7 @@
11. The Infinitude of Primes Nat.exists_infinite_primes (n : ℕ) :
∃ p, n ≤ p ∧ Nat.Prime p
-

docs, source

+

docs, source

@@ -202,7 +202,7 @@
14. Euler’s Summation of 1 + (1/2)^2
theorem hasSum_zeta_two :
HasSum (fun n => 1 / ↑n ^ 2) (Real.pi ^ 2 / 6)
-

docs, source

+

docs, source

@@ -235,7 +235,7 @@
15. Fundamental Theorem of Integral Ca (hb : Filter.Tendsto f (nhds b ⊓ MeasureTheory.Measure.ae MeasureTheory.volume) (nhds c)) :
HasStrictDerivAt (fun u => ∫ (x : ℝ) in a..u, f x) c b
-

docs, source

+

docs, source

theorem intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le @@ -263,7 +263,7 @@
15. Fundamental Theorem of Integral Ca (f'int : IntervalIntegrable f' MeasureTheory.volume a b) :
∫ (y : ℝ) in a..b, f' y = f b - f a
-

docs, source

+

docs, source

@@ -285,7 +285,7 @@
17. De Moivre’s Formula (z : ℂ) :
(Complex.cos z + Complex.sin z * Complex.I) ^ n = Complex.cos (↑n * z) + Complex.sin (↑n * z) * Complex.I
-

docs, source

+

docs, source

@@ -300,7 +300,7 @@
18. Liouville’s Theorem and the Cons (lx : Liouville x) :
Transcendental ℤ x
-

docs, source

+

docs, source

@@ -313,7 +313,7 @@
19. Four Squares Theorem Nat.sum_four_squares (n : ℕ) :
∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n
-

docs, source

+

docs, source

@@ -330,7 +330,7 @@
20. All Primes (1 mod 4) Equal the Sum (hp : p % 4 ≠ 3) :
∃ a b, a ^ 2 + b ^ 2 = p
-

docs, source

+

docs, source

@@ -341,7 +341,7 @@
22. The Non-Denumerability of the Cont
theorem Cardinal.not_countable_real :
¬Set.Countable Set.univ
-

docs, source

+

docs, source

@@ -359,7 +359,7 @@
23. Formula for Pythagorean Triples {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

+

docs, source

@@ -389,7 +389,7 @@
25. Schroeder-Bernstein Theorem (hg : Function.Injective g) :
∃ h, Function.Bijective h
-

docs, source

+

docs, source

@@ -400,7 +400,7 @@
26. Leibniz’s Series for Pi
theorem Real.tendsto_sum_pi_div_four :
Filter.Tendsto (fun k => Finset.sum (Finset.range k) fun i => (-1) ^ i / (2 * ↑i + 1)) Filter.atTop (nhds (Real.pi / 4))
-

docs, source

+

docs, source

@@ -433,7 +433,7 @@
27. Sum of the Angles of a Triangle (h3 : p3 ≠ p1) :
EuclideanGeometry.angle p1 p2 p3 + EuclideanGeometry.angle p2 p3 p1 + EuclideanGeometry.angle p3 p1 p2 = Real.pi
-

docs, source

+

docs, source

@@ -458,7 +458,7 @@
34. Divergence of the Harmonic Series
theorem Real.tendsto_sum_range_one_div_nat_succ_atTop :
Filter.Tendsto (fun n => Finset.sum (Finset.range n) fun i => 1 / (↑i + 1)) Filter.atTop Filter.atTop
-

docs, source

+

docs, source

@@ -484,7 +484,7 @@
35. Taylor’s Theorem (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)) :
∃ x' x_1, f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Set.Icc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(Nat.factorial (n + 1))
-

docs, source

+

docs, source

theorem taylor_mean_remainder_cauchy @@ -503,7 +503,7 @@
35. Taylor’s Theorem (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)) :
∃ x' x_1, f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Set.Icc x₀ x) x' * (x - x') ^ n / ↑(Nat.factorial n) * (x - x₀)
-

docs, source

+

docs, source

@@ -542,7 +542,7 @@
38. Arithmetic Mean/Geometric Mean (hz : ∀ (i : ι), i ∈ s → 0 ≤ z i) :
(Finset.prod s fun i => z i ^ w i) ≤ Finset.sum s fun i => w i * z i
-

docs, source

+

docs, source

@@ -563,7 +563,7 @@
39. Solutions to Pell’s Equation (hp : x * x - Pell.d a1 * y * y = 1) :
∃ n, x = Pell.xn a1 n ∧ y = Pell.yn a1 n
-

docs, source

+

docs, source

theorem Pell.exists_of_not_isSquare @@ -573,7 +573,7 @@
39. Solutions to Pell’s Equation (hd : ¬IsSquare d) :
∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
-

docs, source

+

docs, source

In pell.eq_pell, d is defined to be a*a - 1 for an arbitrary a > 1.

@@ -616,7 +616,7 @@
40. Minkowski’s Fundamental Theorem (h_conv : Convex ℝ s) :
∃ x x_1, ↑x ∈ s
-

docs, source

+

docs, source

@@ -644,7 +644,7 @@
44. The Binomial Theorem (n : ℕ) :
(x + y) ^ n = Finset.sum (Finset.range (n + 1)) fun m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
-

docs, source

+

docs, source

@@ -674,7 +674,7 @@
49. The Cayley-Hamilton Theorem (M : Matrix n n R) :
↑(Polynomial.aeval M) (Matrix.charpoly M) = 0
-

docs, source

+

docs, source

@@ -689,7 +689,7 @@
51. Wilson’s Lemma [Fact (Nat.Prime p)] :
↑(Nat.factorial (p - 1)) = -1
-

docs, source

+

docs, source

@@ -704,7 +704,7 @@
52. The Number of Subsets of a Set (s : Finset α) :
Finset.card (Finset.powerset s) = 2 ^ Finset.card s
-

docs, source

+

docs, source

@@ -750,7 +750,7 @@
55. Product of Segments of Chords (hcpd : EuclideanGeometry.angle c p d = Real.pi) :
dist a p * dist b p = dist c p * dist d p
-

docs, source

+

docs, source

@@ -774,7 +774,7 @@
58. Formula for the Number of Combinat (s : Finset α) :
Finset.card (Finset.powersetCard n s) = Nat.choose (Finset.card s) n
-

docs, source

+

docs, source

theorem Finset.mem_powersetCard @@ -786,7 +786,7 @@
58. Formula for the Number of Combinat {t : Finset α} :
s ∈ Finset.powersetCard n t ↔ s ⊆ t ∧ Finset.card s = n
-

docs, source

+

docs, source

@@ -824,7 +824,7 @@
59. The Laws of Large Numbers (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0)) :
∀ᵐ (ω : Ω), Filter.Tendsto (fun n => (↑n)⁻¹ • Finset.sum (Finset.range n) fun i => X i ω) Filter.atTop (nhds (∫ (a : Ω), X 0 a))
-

docs, source

+

docs, source

@@ -839,7 +839,7 @@
60. Bezout’s Theorem (y : ℕ) :
↑(Nat.gcd x y) = ↑x * Nat.gcdA x y + ↑y * Nat.gcdB x y
-

docs, source

+

docs, source

@@ -871,7 +871,7 @@
62. Fair Games Theorem τ ≤ π → (∃ N, ∀ (x : Ω), π x ≤ N) → ∫ (x : Ω), MeasureTheory.stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), MeasureTheory.stoppedValue f π x ∂μ -

docs, source

+

docs, source

@@ -884,7 +884,7 @@
63. Cantor’s Theorem Cardinal.cantor (a : Cardinal.{u}) :
a < 2 ^ a
-

docs, source

+

docs, source

@@ -913,7 +913,7 @@
64. L’Hopital’s Rule (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

+

docs, source

@@ -944,7 +944,7 @@
65. Isosceles Triangle Theorem (h : dist p1 p2 = dist p1 p3) :
EuclideanGeometry.angle p1 p2 p3 = EuclideanGeometry.angle p1 p3 p2
-

docs, source

+

docs, source

@@ -969,7 +969,7 @@
66. Sum of a Geometric Series (hmn : m ≤ n) :
(Finset.sum (Finset.Ico m n) fun i => x ^ i) = (x ^ n - x ^ m) / (x - 1)
-

docs, source

+

docs, source

theorem NNReal.hasSum_geometric @@ -977,7 +977,7 @@
66. Sum of a Geometric Series (hr : r < 1) :
HasSum (fun n => r ^ n) (1 - r)⁻¹
-

docs, source

+

docs, source

@@ -997,7 +997,7 @@
68. Sum of an arithmetic series Finset.sum_range_id (n : ℕ) :
(Finset.sum (Finset.range n) fun i => i) = n * (n - 1) / 2
-

docs, source

+

docs, source

@@ -1018,7 +1018,7 @@
69. Greatest Common Divisor Algorithm (b : R) :
R
-

docs, source

+

docs, source

theorem EuclideanDomain.gcd_dvd @@ -1032,7 +1032,7 @@
69. Greatest Common Divisor Algorithm (b : R) :
EuclideanDomain.gcd a b ∣ a ∧ EuclideanDomain.gcd a b ∣ b
-

docs, source

+

docs, source

theorem EuclideanDomain.dvd_gcd @@ -1048,7 +1048,7 @@
69. Greatest Common Divisor Algorithm {c : R} :
c ∣ a → c ∣ b → c ∣ EuclideanDomain.gcd a b
-

docs, source

+

docs, source

@@ -1076,7 +1076,7 @@
71. Order of a Subgroup [Fintype { x // x ∈ s }] :
Fintype.card { x // x ∈ s } ∣ Fintype.card α
-

docs, source

+

docs, source

@@ -1101,7 +1101,7 @@
72. Sylow’s Theorem (hdvd : p ^ n ∣ Fintype.card G) :
∃ K, Fintype.card { x // x ∈ K } = p ^ n
-

docs, source

+

docs, source

sylow_conjugate

card_sylow_dvd

card_sylow_modeq_one

@@ -1119,7 +1119,7 @@
74. The Principle of Mathematical Indu
inductive Nat :
Type
-

docs, source

+

docs, source

Automatically generated when defining the natural numbers

@@ -1142,7 +1142,7 @@
75. The Mean Value Theorem (hfd : DifferentiableOn ℝ f (Set.Ioo a b)) :
∃ c, c ∈ Set.Ioo a b ∧ deriv f c = (f b - f a) / (b - a)
-

docs, source

+

docs, source

@@ -1167,7 +1167,7 @@
76. Fourier Series (n : ℤ) :
E
-

docs, source

+

docs, source

theorem hasSum_fourier_series_L2 @@ -1177,7 +1177,7 @@
76. Fourier Series (f : { x // x ∈ MeasureTheory.Lp ℂ 2 }) :
HasSum (fun i => fourierCoeff (↑↑f) i • fourierLp 2 i) f
-

docs, source

+

docs, source

@@ -1192,7 +1192,7 @@
77. Sum of kth powers (p : ℕ) :
(Finset.sum (Finset.range n) fun k => ↑k ^ p) = Finset.sum (Finset.range (p + 1)) fun i => bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / (↑p + 1)
-

docs, source

+

docs, source

theorem sum_Ico_pow @@ -1200,7 +1200,7 @@
77. Sum of kth powers (p : ℕ) :
(Finset.sum (Finset.Ico 1 (n + 1)) fun k => ↑k ^ p) = Finset.sum (Finset.range (p + 1)) fun i => bernoulli' i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / (↑p + 1)
-

docs, source

+

docs, source

@@ -1225,7 +1225,7 @@
78. The Cauchy-Schwarz Inequality (y : E) :
‖inner x y‖ * ‖inner y x‖ ≤ ↑IsROrC.re (inner x x) * ↑IsROrC.re (inner y y)
-

docs, source

+

docs, source

theorem norm_inner_le_norm @@ -1243,7 +1243,7 @@
78. The Cauchy-Schwarz Inequality (y : E) :
‖inner x y‖ ≤ ‖x‖ * ‖y‖
-

docs, source

+

docs, source

@@ -1282,7 +1282,7 @@
79. The Intermediate Value Theorem (hf : ContinuousOn f (Set.Icc a b)) :
Set.Icc (f a) (f b) ⊆ f '' Set.Icc a b
-

docs, source

+

docs, source

@@ -1301,11 +1301,11 @@
80. The Fundamental Theorem of Arithme (h₂ : ∀ (p : ℕ), p ∈ l → Nat.Prime p) :
l ~ Nat.factors n
-

docs, source

+

docs, source

instance Int.euclideanDomain :
EuclideanDomain ℤ
-

docs, source

+

docs, source

instance EuclideanDomain.to_principal_ideal_domain @@ -1313,7 +1313,7 @@
80. The Fundamental Theorem of Arithme [EuclideanDomain R] :
IsPrincipalIdealRing R
-

docs, source

+

docs, source

class UniqueFactorizationMonoid @@ -1323,7 +1323,7 @@
80. The Fundamental Theorem of Arithme extends WfDvdMonoid :
Prop
-

docs, source

+

docs, source

theorem UniqueFactorizationMonoid.factors_unique @@ -1343,7 +1343,7 @@
80. The Fundamental Theorem of Arithme (h : Associated (Multiset.prod f) (Multiset.prod g)) :
Multiset.Rel Associated f g
-

docs, source

+

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.

@@ -1377,7 +1377,7 @@
85. Divisibility by 3 Rule Nat.three_dvd_iff (n : ℕ) :
3 ∣ n ↔ 3 ∣ List.sum (Nat.digits 10 n)
-

docs, source

+

docs, source

@@ -1390,7 +1390,7 @@
86. Lebesgue Measure and Integration < MeasureTheory.lintegral {α : Type u_5} :
{x : MeasurableSpace α} → MeasureTheory.Measure α → (α → ENNReal) → ENNReal
-

docs, source

+

docs, source

@@ -1407,13 +1407,13 @@
88. Derangements Formula [DecidableEq α] :
Fintype.card ↑(derangements α) = numDerangements (Fintype.card α)
-

docs, source

+

docs, source

theorem numDerangements_sum (n : ℕ) :
↑(numDerangements n) = Finset.sum (Finset.range (n + 1)) fun k => (-1) ^ k * ↑(Nat.ascFactorial k (n - k))
-

docs, source

+

docs, source

@@ -1432,7 +1432,7 @@
89. The Factor and Remainder Theorems {p : Polynomial R} :
Polynomial.X - ↑Polynomial.C a ∣ p ↔ Polynomial.IsRoot p a
-

docs, source

+

docs, source

theorem Polynomial.mod_X_sub_C_eq_C_eval @@ -1444,7 +1444,7 @@
89. The Factor and Remainder Theorems (a : R) :
p % (Polynomial.X - ↑Polynomial.C a) = ↑Polynomial.C (Polynomial.eval a p)
-

docs, source

+

docs, source

@@ -1455,7 +1455,7 @@
90. Stirling’s Formula
theorem Stirling.tendsto_stirlingSeq_sqrt_pi :
Filter.Tendsto (fun n => Stirling.stirlingSeq n) Filter.atTop (nhds (Real.sqrt Real.pi))
-

docs, source

+

docs, source

@@ -1474,7 +1474,7 @@
91. The Triangle Inequality (b : E) :
‖a + b‖ ≤ ‖a‖ + ‖b‖
-

docs, source

+

docs, source

@@ -1510,7 +1510,7 @@
94. The Law of Cosines (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

+

docs, source

@@ -1549,7 +1549,7 @@
95. Ptolemy’s Theorem (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

+

docs, source

@@ -1581,7 +1581,7 @@
97. Cramer’s Rule (b : n → α) :
Matrix.mulVec A (↑(Matrix.cramer A) b) = Matrix.det A • b
-

docs, source

+

docs, source

@@ -1596,7 +1596,7 @@
98. Bertrand’s Postulate (hn0 : n ≠ 0) :
∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
-

docs, source

+

docs, source

diff --git a/mathlib_stats.html b/mathlib_stats.html index eb81523f95..7fdfb87101 100644 --- a/mathlib_stats.html +++ b/mathlib_stats.html @@ -80,8 +80,8 @@

Counts

Contributors - 70369 - 126206 + 70411 + 126331 310 diff --git a/teaching/practices.html b/teaching/practices.html index fadd37ab3a..7a69559f5d 100644 --- a/teaching/practices.html +++ b/teaching/practices.html @@ -105,8 +105,7 @@

Organizing course p

Without some kind of structure like this -- for example, if students receive bare .lean files -- it is hard to ensure that they all use the same version of Lean. It is also a good way to provide a "library" file or files -containing basic definitions, tactics, and such that are useful for your course. -[if you are distributing bare Lean files...]

+containing basic definitions, tactics, and such that are useful for your course.

These projects are often hosted on GitHub. Students are asked to clone the project, or create a Codespace or Gitpod instance, at the start of the course.