diff --git a/100.html b/100.html index b1d37e5aa6..aed11c92cf 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

@@ -401,7 +401,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

@@ -434,7 +434,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

@@ -459,7 +459,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

@@ -485,7 +485,7 @@
35. Taylor’s Theorem (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)) :
∃ (x' : ℝ) (_ : x' ∈ Set.Ioo x₀ x), 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 @@ -504,7 +504,7 @@
35. Taylor’s Theorem (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)) :
∃ (x' : ℝ) (_ : x' ∈ Set.Ioo x₀ x), 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

@@ -543,7 +543,7 @@
38. Arithmetic Mean/Geometric Mean (hz : ∀ 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

@@ -564,7 +564,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 @@ -574,7 +574,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.

@@ -617,7 +617,7 @@
40. Minkowski’s Fundamental Theorem (h : ↑↑μ F * 2 ^ FiniteDimensional.finrank ℝ E < ↑↑μ s) :
∃ (x : ↥L), x ≠ 0 ∧ ↑x ∈ s
-

docs, source

+

docs, source

@@ -645,7 +645,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

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

docs, source

+

docs, source

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

docs, source

+

docs, source

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

docs, source

+

docs, source

@@ -751,7 +751,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

@@ -775,7 +775,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 @@ -787,7 +787,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

@@ -826,7 +826,7 @@
59. The Laws of Large Numbers :
∀ᵐ (ω : Ω), 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

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

docs, source

+

docs, source

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

docs, source

+

docs, source

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

docs, source

+

docs, source

@@ -915,7 +915,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) (𝓝[≠] a) l
-

docs, source

+

docs, source

@@ -946,7 +946,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

@@ -971,7 +971,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 @@ -979,7 +979,7 @@
66. Sum of a Geometric Series (hr : r < 1) :
HasSum (fun (n : ℕ) => r ^ n) (1 - r)⁻¹
-

docs, source

+

docs, source

@@ -999,7 +999,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

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

docs, source

+

docs, source

theorem EuclideanDomain.gcd_dvd @@ -1034,7 +1034,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 @@ -1050,7 +1050,7 @@
69. Greatest Common Divisor Algorithm {c : R} :
c ∣ a → c ∣ b → c ∣ EuclideanDomain.gcd a b
-

docs, source

+

docs, source

@@ -1078,7 +1078,7 @@
71. Order of a Subgroup [Fintype ↥s] :
Fintype.card ↥s ∣ Fintype.card α
-

docs, source

+

docs, source

@@ -1103,7 +1103,7 @@
72. Sylow’s Theorem (hdvd : p ^ n ∣ Fintype.card G) :
∃ (K : Subgroup G), Fintype.card ↥K = p ^ n
-

docs, source

+

docs, source

sylow_conjugate

card_sylow_dvd

card_sylow_modeq_one

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

docs, source

+

docs, source

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

docs, source

+

docs, source

theorem hasSum_fourier_series_L2 @@ -1179,7 +1179,7 @@
76. Fourier Series (f : ↥(MeasureTheory.Lp ℂ 2)) :
HasSum (fun (i : ℤ) => fourierCoeff (↑↑f) i • fourierLp 2 i) f
-

docs, source

+

docs, source

@@ -1194,7 +1194,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 @@ -1202,7 +1202,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

@@ -1227,7 +1227,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 @@ -1245,7 +1245,7 @@
78. The Cauchy-Schwarz Inequality (y : E) :
‖inner x y‖ ≤ ‖x‖ * ‖y‖
-

docs, source

+

docs, source

@@ -1284,7 +1284,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

@@ -1303,11 +1303,11 @@
80. The Fundamental Theorem of Arithme (h₂ : ∀ 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 @@ -1315,7 +1315,7 @@
80. The Fundamental Theorem of Arithme [EuclideanDomain R] :
IsPrincipalIdealRing R
-

docs, source

+

docs, source

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

docs, source

+

docs, source

theorem UniqueFactorizationMonoid.factors_unique @@ -1345,7 +1345,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.

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

docs, source

+

docs, source

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

docs, source

+

docs, source

@@ -1409,13 +1409,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

@@ -1434,7 +1434,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 @@ -1446,7 +1446,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

@@ -1457,7 +1457,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

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

docs, source

+

docs, source

@@ -1512,7 +1512,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

@@ -1551,7 +1551,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

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

docs, source

+

docs, source

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

docs, source

+

docs, source

diff --git a/lean_projects.html b/lean_projects.html index 083c9c9aa8..a10a5a4e52 100644 --- a/lean_projects.html +++ b/lean_projects.html @@ -308,7 +308,7 @@
maintained by

- View on GitHub (★ 31) + View on GitHub (★ 36)
@@ -394,21 +394,19 @@
maintained by
-
rubiks-cube-group
+
con-nf
maintained by - @kendfrey + @YaelDillies + + @zeramorphic
-

This project formalizes the Rubik's cube group as a product of corner orientation, -corner permutation, edge orientation, and edge permutation.

-

The solvable subgroup is defined as the the set of positions where both orientations sum -to 0 and the permutations have the same sign.

-

This project includes a widget to visualize elements of the group as physical puzzle states.

+

A formalisation of the consistency of Quine's New Foundations axiom system, following Randall Holmes' proof. This is arguably the longest standing open question in set theory.

- View on GitHub (★ 19) + View on GitHub (★ 20)
@@ -416,19 +414,21 @@
maintained by
-
con-nf
+
rubiks-cube-group
maintained by - @YaelDillies - - @zeramorphic + @kendfrey
-

A formalisation of the consistency of Quine's New Foundations axiom system, following Randall Holmes' proof. This is arguably the longest standing open question in set theory.

+

This project formalizes the Rubik's cube group as a product of corner orientation, +corner permutation, edge orientation, and edge permutation.

+

The solvable subgroup is defined as the the set of positions where both orientations sum +to 0 and the permutations have the same sign.

+

This project includes a widget to visualize elements of the group as physical puzzle states.

- View on GitHub (★ 19) + View on GitHub (★ 19)
diff --git a/mathlib-overview.html b/mathlib-overview.html index a6cc12f93e..fe3ce8e55c 100644 --- a/mathlib-overview.html +++ b/mathlib-overview.html @@ -520,11 +520,11 @@

Linear algebra Bilinear and quadratic forms - bilinear form, + bilinear form, - alternating bilinear form, + alternating bilinear form, - symmetric bilinear form, + symmetric bilinear form, matrix representation, diff --git a/mathlib_stats.html b/mathlib_stats.html index ac2bbc5443..1619ec0afe 100644 --- a/mathlib_stats.html +++ b/mathlib_stats.html @@ -60,8 +60,8 @@

Counts

Contributors - 72502 - 130881 + 72527 + 130923 310 diff --git a/undergrad.html b/undergrad.html index 6fc5fa34da..deda371e39 100644 --- a/undergrad.html +++ b/undergrad.html @@ -452,13 +452,13 @@

Bilinear and Quadratic Forms Over a Vector Space

Bilinear forms - bilinear forms, + bilinear forms, - alternating bilinear forms, + alternating bilinear forms, - symmetric bilinear forms, + symmetric bilinear forms, - nondegenerate forms, + nondegenerate forms, matrix representation, @@ -478,9 +478,9 @@

Bilinear and Quadratic Forms Over a Vector Space

Orthogonality - orthogonal elements, + orthogonal elements, - adjoint endomorphism, + adjoint endomorphism, Gram-Schmidt orthogonalisation.