From 55ae28a6363026145f1eae23d2bdc826e3d2e677 Mon Sep 17 00:00:00 2001 From: leanprover-community-bot Date: Fri, 17 Jan 2025 04:07:58 +0000 Subject: [PATCH] deploy site from ff63c363a87c65a1e4b0acedf6450b88fc91e0a5 --- 100.html | 200 +++++------ 1000.html | 314 ++++++++--------- lean_projects.html | 32 +- mathlib_stats.html | 4 +- meet.html | 852 ++++++++++++++++++++++----------------------- 5 files changed, 701 insertions(+), 701 deletions(-) diff --git a/100.html b/100.html index f3ce63603..37e1b0064 100644 --- a/100.html +++ b/100.html @@ -70,7 +70,7 @@
1. The Irrationality of the Square Root
theorem irrational_sqrt_two :
Irrational √2
-

docs, source

+

docs, source

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

docs, source

+

docs, source

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

docs, source

+

docs, source

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

@@ -151,7 +151,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 @@ -161,7 +161,7 @@
7. Law of Quadratic Reciprocity (hb : Odd b) :
jacobiSym (↑a) b = (-1) ^ (a / 2 * (b / 2)) * jacobiSym (↑b) a
-

docs, source

+

docs, source

@@ -174,7 +174,7 @@
9. The Area of a Circle Theorems100.area_disc (r : NNReal) :
MeasureTheory.volume (Theorems100.disc ↑r) = ↑NNReal.pi * ↑r ^ 2
-

docs, source

+

docs, source

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

docs, source

+

docs, source

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

docs, source

+

docs, source

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

@@ -244,7 +244,7 @@
15. Fundamental Theorem of Integral Ca (hb : Filter.Tendsto f (nhds b ⊓ MeasureTheory.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 @@ -268,7 +268,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

@@ -279,7 +279,7 @@
16. Insolvability of General Higher De
theorem AbelRuffini.exists_not_solvable_by_rad :
∃ (x : ℂ), IsAlgebraic ℚ x ∧ ¬IsSolvableByRad ℚ x
-

docs, source

+

docs, source

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

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

docs, source

+

docs, source

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

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

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

docs, source

+

docs, source

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

docs, source

+

docs, source

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

docs, source

+

docs, source

@@ -405,7 +405,7 @@
26. Leibniz’s Series for Pi
theorem 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))
-

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

@@ -447,7 +447,7 @@
30. The Ballot Problem Ballot.ballot_problem (q p : ℕ) :
q < p → (ProbabilityTheory.uniformOn (Ballot.countedSequence p q)) Ballot.staysPositive = (↑p - ↑q) / (↑p + ↑q)
-

docs, source

+

docs, source

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

docs, source

+

docs, source

@@ -489,7 +489,7 @@
35. Taylor’s Theorem (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo 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) / ↑(n + 1).factorial
-

docs, source

+

docs, source

theorem taylor_mean_remainder_cauchy @@ -506,7 +506,7 @@
35. Taylor’s Theorem (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo 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 / ↑n.factorial * (x - x₀)
-

docs, source

+

docs, source

@@ -554,7 +554,7 @@
37. The Solution of a Cubic (x : K) :
a * x ^ 3 + b * x ^ 2 + c * x + d = 0 ↔ x = s - t - b / (3 * a) ∨ x = s * ω - t * ω ^ 2 - b / (3 * a) ∨ x = s * ω ^ 2 - t * ω - b / (3 * a)
-

docs, source

+

docs, source

@@ -577,7 +577,7 @@
38. Arithmetic Mean/Geometric Mean (hz : ∀ i ∈ s, 0 ≤ z i) :
∏ i ∈ s, z i ^ w i ≤ ∑ i ∈ s, w i * z i
-

docs, source

+

docs, source

@@ -596,7 +596,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 @@ -606,7 +606,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.

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

docs, source

+

docs, source

@@ -660,7 +660,7 @@
42. Sum of the Reciprocals of the Tria Theorems100.inverse_triangle_sum (n : ℕ) :
∑ k ∈ Finset.range n, 2 / (↑k * (↑k + 1)) = if n = 0 then 0 else 2 - 2 / ↑n
-

docs, source

+

docs, source

@@ -679,7 +679,7 @@
44. The Binomial Theorem (n : ℕ) :
(x + y) ^ n = ∑ m ∈ Finset.range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)
-

docs, source

+

docs, source

@@ -692,7 +692,7 @@
45. The Partition Theorem Theorems100.partition_theorem (n : ℕ) :
(Nat.Partition.odds n).card = (Nat.Partition.distincts n).card
-

docs, source

+

docs, source

@@ -733,7 +733,7 @@
46. The Solution of the General Quarti (x : K) :
a * x ^ 4 + b * x ^ 3 + c * x ^ 2 + d * x + e = 0 ↔ x = (-2 * s - v) / 4 - b / (4 * a) ∨ x = (-2 * s + v) / 4 - b / (4 * a) ∨ x = (2 * s - w) / 4 - b / (4 * a) ∨ x = (2 * s + w) / 4 - b / (4 * a)
-

docs, source

+

docs, source

@@ -752,7 +752,7 @@
48. Dirichlet’s Theorem (ha : IsUnit a) :
{p : ℕ | Nat.Prime p ∧ ↑p = a}.Infinite
-

docs, source

+

docs, source

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

docs, source

+

docs, source

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

docs, source

+

docs, source

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

docs, source

+

docs, source

@@ -822,7 +822,7 @@
54. Königsberg Bridges Problem (h : p.IsEulerian) :
False
-

docs, source

+

docs, source

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

@@ -886,7 +886,7 @@
57. Heron’s Formula let c := dist p1 p3; let s := (a + b + c) / 2; 1 / 2 * a * b * Real.sin (EuclideanGeometry.angle p1 p2 p3) = √(s * (s - a) * (s - b) * (s - c)) -

docs, source

+

docs, source

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

docs, source

+

docs, source

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

docs, source

+

docs, source

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

docs, source

+

docs, source

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

docs, source

+

docs, source

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

docs, source

+

docs, source

@@ -1011,7 +1011,7 @@
63. Cantor’s Theorem (f : α → Set α) :
¬Function.Surjective f
-

docs, source

+

docs, source

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

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

@@ -1088,7 +1088,7 @@
66. Sum of a Geometric Series (hmn : m ≤ n) :
∑ i ∈ Finset.Ico m n, x ^ i = (x ^ n - x ^ m) / (x - 1)
-

docs, source

+

docs, source

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

docs, source

+

docs, source

@@ -1116,7 +1116,7 @@
68. Sum of an arithmetic series Finset.sum_range_id (n : ℕ) :
∑ i ∈ Finset.range n, i = n * (n - 1) / 2
-

docs, source

+

docs, source

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

docs, source

+

docs, source

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

docs, source

+

docs, source

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

docs, source

+

docs, source

@@ -1176,7 +1176,7 @@
70. The Perfect Number Theorem (perf : n.Perfect) :
∃ (k : ℕ), Nat.Prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1)
-

docs, source

+

docs, source

@@ -1193,7 +1193,7 @@
71. Order of a Subgroup (s : Subgroup α) :
Nat.card ↥s ∣ Nat.card α
-

docs, source

+

docs, source

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

docs, source

+

docs, source

instance Sylow.isPretransitive_of_finite @@ -1232,7 +1232,7 @@
72. Sylow’s Theorem [Finite (Sylow p G)] :
MulAction.IsPretransitive G (Sylow p G)
-

docs, source

+

docs, source

theorem Sylow.card_dvd_index @@ -1248,7 +1248,7 @@
72. Sylow’s Theorem (P : Sylow p G) :
Nat.card (Sylow p G) ∣ (↑P).index
-

docs, source

+

docs, source

theorem card_sylow_modEq_one @@ -1262,7 +1262,7 @@
72. Sylow’s Theorem [Finite (Sylow p G)] :
Nat.card (Sylow p G) ≡ 1 [MOD p]
-

docs, source

+

docs, source

@@ -1285,7 +1285,7 @@
73. Ascending or Descending Sequences (hf : Function.Injective f) :
(∃ (t : Finset (Fin n)), r < t.card ∧ StrictMonoOn f ↑t) ∨ ∃ (t : Finset (Fin n)), s < t.card ∧ StrictAntiOn f ↑t
-

docs, source

+

docs, source

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

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

docs, source

+

docs, source

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

docs, source

+

docs, source

@@ -1365,13 +1365,13 @@
77. Sum of kth powers sum_range_pow (n p : ℕ) :
∑ k ∈ Finset.range n, ↑k ^ p = ∑ i ∈ Finset.range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)
-

docs, source

+

docs, source

theorem sum_Ico_pow (n p : ℕ) :
∑ k ∈ Finset.Ico 1 (n + 1), ↑k ^ p = ∑ i ∈ Finset.range (p + 1), bernoulli' i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)
-

docs, source

+

docs, source

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

docs, source

+

docs, source

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

docs, source

+

docs, source

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

@@ -1466,11 +1466,11 @@
80. The Fundamental Theorem of Arithme (h₂ : ∀ p ∈ l, Nat.Prime p) :
l.Perm n.primeFactorsList
-

docs, source

+

docs, source

instance Int.euclideanDomain :
EuclideanDomain ℤ
-

docs, source

+

docs, source

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

docs, source

+

docs, source

class UniqueFactorizationMonoid @@ -1486,7 +1486,7 @@
80. The Fundamental Theorem of Arithme [CancelCommMonoidWithZero α] extends IsWellFounded α DvdNotUnit :
Prop
-

docs, source

+

docs, source

theorem UniqueFactorizationMonoid.factors_unique @@ -1504,7 +1504,7 @@
80. The Fundamental Theorem of Arithme (h : Associated f.prod g.prod) :
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.

@@ -1516,11 +1516,11 @@
81. Divergence of the Prime Reciprocal
theorem Theorems100.Real.tendsto_sum_one_div_prime_atTop :
Filter.Tendsto (fun (n : ℕ) => ∑ p ∈ Finset.filter (fun (p : ℕ) => Nat.Prime p) (Finset.range n), 1 / ↑p) Filter.atTop Filter.atTop
-

docs, source

+

docs, source

theorem not_summable_one_div_on_primes :
¬Summable ({p : ℕ | Nat.Prime p}.indicator fun (n : ℕ) => 1 / ↑n)
-

docs, source

+

docs, source

@@ -1538,7 +1538,7 @@
82. Dissection of Cubes (J.E. Littlewo 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 -

docs, source

+

docs, source

@@ -1559,7 +1559,7 @@
83. The Friendship Theorem [Nonempty V] :
Theorems100.ExistsPolitician G
-

docs, source

+

docs, source

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

docs, source

+

docs, source

@@ -1591,7 +1591,7 @@
86. Lebesgue Measure and Integration < (f : α → ENNReal) :
ENNReal
-

docs, source

+

docs, source

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

docs, source

+

docs, source

theorem numDerangements_sum (n : ℕ) :
↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
-

docs, source

+

docs, source

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

docs, source

+

docs, source

theorem Polynomial.mod_X_sub_C_eq_C_eval @@ -1645,7 +1645,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

@@ -1656,7 +1656,7 @@
90. Stirling’s Formula
theorem Stirling.tendsto_stirlingSeq_sqrt_pi :
Filter.Tendsto Stirling.stirlingSeq Filter.atTop (nhds √Real.pi)
-

docs, source

+

docs, source

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

docs, source

+

docs, source

@@ -1684,11 +1684,11 @@
93. The Birthday Problem
theorem 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)
-

docs, source

+

docs, source

theorem Theorems100.birthday_measure :
MeasureTheory.volume {f : Fin 23 → Fin 365 | Function.Injective f} < 1 / 2
-

docs, source

+

docs, source

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

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

@@ -1772,7 +1772,7 @@
96. Principle of Inclusion/Exclusion < (f : α → G) :
∑ a ∈ s.biUnion S, f a = ∑ t : { x : Finset ι // x ∈ Finset.filter (fun (x : Finset ι) => x.Nonempty) s.powerset }, (-1) ^ ((↑t).card + 1) • ∑ a ∈ (↑t).inf' ⋯ S, f a
-

docs, source

+

docs, source

theorem Finset.inclusion_exclusion_card_biUnion @@ -1787,7 +1787,7 @@
96. Principle of Inclusion/Exclusion < (S : ι → Finset α) :
↑(s.biUnion S).card = ∑ t : { x : Finset ι // x ∈ Finset.filter (fun (x : Finset ι) => x.Nonempty) s.powerset }, (-1) ^ ((↑t).card + 1) * ↑((↑t).inf' ⋯ S).card
-

docs, source

+

docs, source

theorem Finset.inclusion_exclusion_sum_inf_compl @@ -1809,7 +1809,7 @@
96. Principle of Inclusion/Exclusion < (f : α → G) :
∑ a ∈ s.inf fun (i : ι) => (S i)ᶜ, f a = ∑ t ∈ s.powerset, (-1) ^ t.card • ∑ a ∈ t.inf S, f a
-

docs, source

+

docs, source

theorem Finset.inclusion_exclusion_card_inf_compl @@ -1825,7 +1825,7 @@
96. Principle of Inclusion/Exclusion < (S : ι → Finset α) :
↑(s.inf fun (i : ι) => (S i)ᶜ).card = ∑ t ∈ s.powerset, (-1) ^ t.card * ↑(t.inf S).card
-

docs, source

+

docs, source

github

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

docs, source

+

docs, source

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

docs, source

+

docs, source

@@ -1896,7 +1896,7 @@
99. Buffon Needle Problem (h : l ≤ d) :
∫ (x : Ω), BuffonsNeedle.N l B x = 2 * l * (d * Real.pi)⁻¹
-

docs, source

+

docs, source

theorem BuffonsNeedle.buffon_long @@ -1920,7 +1920,7 @@
99. Buffon Needle Problem (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
-

docs, source

+

docs, source

diff --git a/1000.html b/1000.html index 77cb5a199..6236444a3 100644 --- a/1000.html +++ b/1000.html @@ -84,7 +84,7 @@
Q11518: Pythagorean theorem (p1 p2 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

@@ -103,7 +103,7 @@
Q26708: Binomial theorem (n : ℕ) :
(x + y) ^ n = ∑ m ∈ Finset.range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)
-

docs, source

+

docs, source

@@ -148,7 +148,7 @@
Q137164: Besicovitch covering the (hR : ∀ x ∈ s, 0 < R x) :
∃ (t : Set α) (r : α → ℝ), t.Countable ∧ t ⊆ s ∧ (∀ x ∈ t, r x ∈ f x ∩ Set.Ioo 0 (R x)) ∧ μ (s \ ⋃ x ∈ t, Metric.closedBall x (r x)) = 0 ∧ t.PairwiseDisjoint fun (x : α) => Metric.closedBall x (r x)
-

docs, source

+

docs, source

@@ -169,7 +169,7 @@
Q179208: Cayley's theorem [FaithfulSMul G H] :
G ≃* ↥(MulAction.toPermHom G H).range
-

docs, source

+

docs, source

@@ -194,7 +194,7 @@
Q182505: Bayes' theorem [MeasureTheory.IsFiniteMeasure μ] :
(ProbabilityTheory.cond μ s) t = (μ s)⁻¹ * (ProbabilityTheory.cond μ t) s * μ t
-

docs, source

+

docs, source

@@ -213,7 +213,7 @@
Q188295: Fermat's little theorem (ha : a ≠ 0) :
a ^ (p - 1) = 1
-

docs, source

+

docs, source

@@ -234,7 +234,7 @@
Q189136: 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

theorem exists_ratio_deriv_eq_ratio_slope @@ -254,7 +254,7 @@
Q189136: Mean value theorem (hgd : DifferentiableOn ℝ g (Set.Ioo a b)) :
∃ c ∈ Set.Ioo a b, (g b - g a) * deriv f c = (f b - f a) * deriv g c
-

docs, source

+

docs, source

@@ -269,7 +269,7 @@
Q190556: De Moivre's theorem (z : ℂ) :
(Complex.cos z + Complex.sin z * Complex.I) ^ n = Complex.cos (↑n * z) + Complex.sin (↑n * z) * Complex.I
-

docs, source

+

docs, source

@@ -290,7 +290,7 @@
Q191693: Lebesgue's decomposition [MeasureTheory.SigmaFinite ν] :
μ.HaveLebesgueDecomposition ν
-

docs, source

+

docs, source

@@ -301,7 +301,7 @@
Q192760: Fundamental theorem of a
instance Complex.isAlgClosed :
IsAlgClosed ℂ
-

docs, source

+

docs, source

@@ -322,7 +322,7 @@
Q193286: Rolle's theorem (hfI : f a = f b) :
∃ c ∈ Set.Ioo a b, deriv f c = 0
-

docs, source

+

docs, source

@@ -345,7 +345,7 @@
Q193878: Chinese remainder theore (hf : Pairwise (Function.onFun IsCoprime f)) :
R ⧸ ⨅ (i : ι), f i ≃+* ((i : ι) → R ⧸ f i)
-

docs, source

+

docs, source

@@ -393,7 +393,7 @@
Q203565: Solutions of a general c (x : K) :
a * x ^ 3 + b * x ^ 2 + c * x + d = 0 ↔ x = s - t - b / (3 * a) ∨ x = s * ω - t * ω ^ 2 - b / (3 * a) ∨ x = s * ω ^ 2 - t * ω - b / (3 * a)
-

docs, source

+

docs, source

@@ -428,7 +428,7 @@
Q220680: Banach fixed-point theor (hx : edist x (f x) ≠ ⊤) :
∃ (y : α), Function.IsFixedPt f y ∧ Filter.Tendsto (fun (n : ℕ) => f^[n] x) Filter.atTop (nhds y) ∧ ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
-

docs, source

+

docs, source

@@ -465,7 +465,7 @@
Q245098: Intermediate value theor (hf : ContinuousOn f (Set.Icc a b)) :
Set.Icc (f a) (f b) ⊆ f '' Set.Icc a b
-

docs, source

+

docs, source

@@ -486,7 +486,7 @@
Q253214: Heine–Borel theorem [ProperSpace α] :
IsCompact s ↔ IsClosed s ∧ Bornology.IsBounded s
-

docs, source

+

docs, source

theorem FiniteDimensional.proper @@ -504,7 +504,7 @@
Q253214: Heine–Borel theorem [FiniteDimensional 𝕜 E] :
ProperSpace E
-

docs, source

+

docs, source

@@ -519,7 +519,7 @@
Q276082: Wilson's theorem [Fact (Nat.Prime p)] :
↑(p - 1).factorial = -1
-

docs, source

+

docs, source

@@ -540,7 +540,7 @@
Q288465: Orbit-stabilizer theorem (b : β) :
↑(MulAction.orbit α b) ≃ α ⧸ MulAction.stabilizer α b
-

docs, source

+

docs, source

@@ -569,7 +569,7 @@
Q303402: Rank–nullity theorem < (f : M →ₗ[R] M₁) :
Module.rank R ↥(LinearMap.range f) + Module.rank R ↥(LinearMap.ker f) = Module.rank R M
-

docs, source

+

docs, source

@@ -590,7 +590,7 @@
Q318767: Abel's theorem (hs : 0 < s) :
Filter.Tendsto (fun (z : ℂ) => ∑' (n : ℕ), f n * z ^ n) (nhdsWithin 1 (Complex.stolzCone s)) (nhds l)
-

docs, source

+

docs, source

theorem Real.tendsto_tsum_powerSeries_nhdsWithin_lt @@ -600,7 +600,7 @@
Q318767: Abel's theorem (h : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds l)) :
Filter.Tendsto (fun (x : ℝ) => ∑' (n : ℕ), f n * x ^ n) (nhdsWithin 1 (Set.Iio 1)) (nhds l)
-

docs, source

+

docs, source

@@ -627,7 +627,7 @@
Q420714: Akra–Bazzi theorem (R : AkraBazziRecurrence T g a b r) :
T =O[Filter.atTop] AkraBazziRecurrence.asympBound g a b
-

docs, source

+

docs, source

@@ -658,7 +658,7 @@
Q459547: 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

@@ -683,7 +683,7 @@
Q468391: Bolzano–Weierstrass th (hx : ∃ᶠ (n : ℕ) in Filter.atTop, x n ∈ s) :
∃ a ∈ closure s, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)
-

docs, source

+

docs, source

theorem tendsto_subseq_of_bounded @@ -701,7 +701,7 @@
Q468391: Bolzano–Weierstrass th (hx : ∀ (n : ℕ), x n ∈ s) :
∃ a ∈ closure s, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)
-

docs, source

+

docs, source

@@ -712,7 +712,7 @@
Q470877: Stirling's theorem
theorem Stirling.tendsto_stirlingSeq_sqrt_pi :
Filter.Tendsto Stirling.stirlingSeq Filter.atTop (nhds √Real.pi)
-

docs, source

+

docs, source

@@ -735,7 +735,7 @@
Q472883: Quadratic reciprocity th (hpq : p ≠ q) :
legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
-

docs, source

+

docs, source

theorem jacobiSym.quadratic_reciprocity @@ -745,7 +745,7 @@
Q472883: Quadratic reciprocity th (hb : Odd b) :
jacobiSym (↑a) b = (-1) ^ (a / 2 * (b / 2)) * jacobiSym (↑b) a
-

docs, source

+

docs, source

@@ -760,7 +760,7 @@
Q474881: Cantor's theorem (f : α → Set α) :
¬Function.Surjective f
-

docs, source

+

docs, source

@@ -801,7 +801,7 @@
Q476776: Solutions of a general q (x : K) :
a * x ^ 4 + b * x ^ 3 + c * x ^ 2 + d * x + e = 0 ↔ x = (-2 * s - v) / 4 - b / (4 * a) ∨ x = (-2 * s + v) / 4 - b / (4 * a) ∨ x = (2 * s - w) / 4 - b / (4 * a) ∨ x = (2 * s + w) / 4 - b / (4 * a)
-

docs, source

+

docs, source

@@ -818,7 +818,7 @@
Q505798: Lagrange's theorem (s : Subgroup α) :
Nat.card ↥s ∣ Nat.card α
-

docs, source

+

docs, source

@@ -849,7 +849,7 @@
Q530152: Picard–Lindelöf t (hpl : IsPicardLindelof v tMin t₀ tMax x₀ L R C) :
∃ (f : ℝ → E), f t₀ = x₀ ∧ ∀ t ∈ Set.Icc tMin tMax, HasDerivWithinAt f (v t (f t)) (Set.Icc tMin tMax) t
-

docs, source

+

docs, source

@@ -868,7 +868,7 @@
Q536640: Hall's marriage theorem (t : ι → Finset α) :
(∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) ↔ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
-

docs, source

+

docs, source

@@ -895,7 +895,7 @@
Q537618: Banach–Alaoglu theorem (s_nhd : s ∈ nhds 0) :
IsCompact (WeakDual.polar 𝕜 s)
-

docs, source

+

docs, source

@@ -914,7 +914,7 @@
Q550402: Dirichlet's theorem on a (ha : IsUnit a) :
{p : ℕ | Nat.Prime p ∧ ↑p = a}.Infinite
-

docs, source

+

docs, source

@@ -931,7 +931,7 @@
Q570779: Vieta's formulas (s : Multiset R) :
(Multiset.map (fun (r : R) => Polynomial.X + Polynomial.C r) s).prod = ∑ j ∈ Finset.range (s.card + 1), Polynomial.C (s.esymm j) * Polynomial.X ^ (s.card - j)
-

docs, source

+

docs, source

@@ -962,7 +962,7 @@
Q576478: Liouville's theorem (z w : E) :
f z = f w
-

docs, source

+

docs, source

@@ -979,7 +979,7 @@
Q609612: Knaster–Tarski theorem (f : α →o α) :
CompleteLattice ↑(Function.fixedPoints ⇑f)
-

docs, source

+

docs, source

@@ -1006,7 +1006,7 @@
Q619985: Multinomial theorem (n : ℕ) :
(∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(Nat.multinomial s k) * s.noncommProd (fun (i : α) => f i ^ k i) ⋯
-

docs, source

+

docs, source

@@ -1021,7 +1021,7 @@
Q632546: Bertrand's postulate (hn0 : n ≠ 0) :
∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
-

docs, source

+

docs, source

@@ -1054,7 +1054,7 @@
Q642620: Krein–Milman theorem < (hAconv : Convex ℝ s) :
closure ((convexHull ℝ) (Set.extremePoints ℝ s)) = s
-

docs, source

+

docs, source

@@ -1077,7 +1077,7 @@
Q656772: Cayley–Hamilton theore (M : Matrix n n R) :
(Polynomial.aeval M) M.charpoly = 0
-

docs, source

+

docs, source

@@ -1088,7 +1088,7 @@
Q657482: Abel–Ruffini theorem <
theorem AbelRuffini.exists_not_solvable_by_rad :
∃ (x : ℂ), IsAlgebraic ℚ x ∧ ¬IsSolvableByRad ℚ x
-

docs, source

+

docs, source

@@ -1107,11 +1107,11 @@
Q670235: Fundamental theorem of a (h₂ : ∀ p ∈ l, Nat.Prime p) :
l.Perm n.primeFactorsList
-

docs, source

+

docs, source

instance Int.euclideanDomain :
EuclideanDomain ℤ
-

docs, source

+

docs, source

instance EuclideanDomain.to_principal_ideal_domain @@ -1119,7 +1119,7 @@
Q670235: Fundamental theorem of a [EuclideanDomain R] :
IsPrincipalIdealRing R
-

docs, source

+

docs, source

class UniqueFactorizationMonoid @@ -1127,7 +1127,7 @@
Q670235: Fundamental theorem of a [CancelCommMonoidWithZero α] extends IsWellFounded α DvdNotUnit :
Prop
-

docs, source

+

docs, source

theorem UniqueFactorizationMonoid.factors_unique @@ -1145,7 +1145,7 @@
Q670235: Fundamental theorem of a (h : Associated f.prod g.prod) :
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.

@@ -1166,7 +1166,7 @@
Q716171: Erdős–Ginzburg–Ziv (hs : 2 * n - 1 ≤ s.card) :
∃ t ⊆ s, t.card = n ∧ ∑ i ∈ t, a i = 0
-

docs, source

+

docs, source

@@ -1189,7 +1189,7 @@
Q718875: Erdős–Ko–Rado theor (h₃ : r ≤ n / 2) :
𝒜.card ≤ (n - 1).choose (r - 1)
-

docs, source

+

docs, source

@@ -1226,7 +1226,7 @@
Q720469: Chevalley–Warning theo (h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ) :
p ∣ Fintype.card { x : σ → K // ∀ i ∈ s, (MvPolynomial.eval x) (f i) = 0 }
-

docs, source

+

docs, source

@@ -1266,7 +1266,7 @@
Q752375: Extreme value theorem (hf : ContinuousOn f s) :
∃ x ∈ s, IsMinOn f s x
-

docs, source

+

docs, source

@@ -1279,7 +1279,7 @@
Q756946: Lagrange's four-square t Nat.sum_four_squares (n : ℕ) :
∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ), a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n
-

docs, source

+

docs, source

@@ -1302,7 +1302,7 @@
Q764287: Van der Waerden's theore (C : M → κ) :
∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c
-

docs, source

+

docs, source

@@ -1327,7 +1327,7 @@
Q765987: Heine–Cantor theorem < (h : Continuous f) :
UniformContinuous f
-

docs, source

+

docs, source

@@ -1354,7 +1354,7 @@
Q834025: Cauchy integral theorem (hd : ∀ z ∈ Metric.ball c R \ s, DifferentiableAt ℂ f z) :
(∮ (z : ℂ) in C(c, R), f z / (z - w)) = 2 * ↑Real.pi * Complex.I * f w
-

docs, source

+

docs, source

@@ -1392,7 +1392,7 @@
Q842953: Lebesgue's density theor :
∀ᵐ (x : β) ∂μ.restrict s, Filter.Tendsto (fun (r : ℝ) => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)
-

docs, source

+

docs, source

@@ -1433,7 +1433,7 @@
Q848375: Implicit function theore (φ : ImplicitFunctionData 𝕜 E F G) :
F → G → E
-

docs, source

+

docs, source

@@ -1452,7 +1452,7 @@
Q853067: Solutions to Pell's equa (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 @@ -1462,7 +1462,7 @@
Q853067: Solutions to Pell's equa (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.

@@ -1489,7 +1489,7 @@
Q866116: Hahn–Banach theorem (f : ↥p →L[𝕜] 𝕜) :
∃ (g : E →L[𝕜] 𝕜), (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖
-

docs, source

+

docs, source

@@ -1506,7 +1506,7 @@
Q914517: Fermat's theorem on sums (hp : p % 4 ≠ 3) :
∃ (a : ℕ) (b : ℕ), a ^ 2 + b ^ 2 = p
-

docs, source

+

docs, source

@@ -1550,7 +1550,7 @@
Q931001: Inverse function theorem (hf : HasStrictFDerivAt f (↑f') a) :
HasStrictFDerivAt (HasStrictFDerivAt.localInverse f f' a hf) (↑f'.symm) (f a)
-

docs, source

+

docs, source

@@ -1571,7 +1571,7 @@
Q939927: Stone–Weierstrass theo (w : A.SeparatesPoints) :
A.topologicalClosure = ⊤
-

docs, source

+

docs, source

@@ -1588,7 +1588,7 @@
Q943246: Wedderburn's little theo [Finite D] :
Field D
-

docs, source

+

docs, source

@@ -1620,7 +1620,7 @@
Q967972: Open mapping theorem (hU : IsPreconnected U) :
(∃ (w : ℂ), ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen s → IsOpen (g '' s)
-

docs, source

+

docs, source

@@ -1643,7 +1643,7 @@
Q976607: Erdős–Szekeres theore (hf : Function.Injective f) :
(∃ (t : Finset (Fin n)), r < t.card ∧ StrictMonoOn f ↑t) ∨ ∃ (t : Finset (Fin n)), s < t.card ∧ StrictAntiOn f ↑t
-

docs, source

+

docs, source

@@ -1662,7 +1662,7 @@
Q1032886: Hales–Jewett theorem [Finite κ] :
∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Combinatorics.Line α ι), Combinatorics.Line.IsMono C l
-

docs, source

+

docs, source

@@ -1685,7 +1685,7 @@
Q1033910: Cantor–Bernstein–S (hg : Function.Injective g) :
∃ (h : α → β), Function.Bijective h
-

docs, source

+

docs, source

@@ -1722,7 +1722,7 @@
Q1038716: Identity theorem (hfg : ∃ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z = g z) :
Set.EqOn f g U
-

docs, source

+

docs, source

@@ -1745,7 +1745,7 @@
Q1047749: Turán's theorem (hr : 0 < r) :
G.IsTuranMaximal r ↔ Nonempty (G ≃g SimpleGraph.turanGraph (Fintype.card V) r)
-

docs, source

+

docs, source

@@ -1772,7 +1772,7 @@
Q1050203: Cantor's intersection (hScl : ∀ U ∈ S, IsClosed U) :
(⋂₀ S).Nonempty
-

docs, source

+

docs, source

@@ -1804,7 +1804,7 @@
Q1052678: Baire category theorem (hd : ∀ s ∈ S, Dense s) :
Dense (⋂₀ S)
-

docs, source

+

docs, source

@@ -1829,7 +1829,7 @@
Q1057919: Sylow theorems (hdvd : p ^ n ∣ Nat.card G) :
∃ (K : Subgroup G), Nat.card ↥K = p ^ n
-

docs, source

+

docs, source

instance Sylow.isPretransitive_of_finite @@ -1843,7 +1843,7 @@
Q1057919: Sylow theorems [Finite (Sylow p G)] :
MulAction.IsPretransitive G (Sylow p G)
-

docs, source

+

docs, source

theorem Sylow.card_dvd_index @@ -1859,7 +1859,7 @@
Q1057919: Sylow theorems (P : Sylow p G) :
Nat.card (Sylow p G) ∣ (↑P).index
-

docs, source

+

docs, source

theorem card_sylow_modEq_one @@ -1873,7 +1873,7 @@
Q1057919: Sylow theorems [Finite (Sylow p G)] :
Nat.card (Sylow p G) ≡ 1 [MOD p]
-

docs, source

+

docs, source

@@ -1908,7 +1908,7 @@
Q1065257: Squeeze theorem (hfh : ∀ᶠ (b : β) in b, f b ≤ h b) :
Filter.Tendsto f b (nhds a)
-

docs, source

+

docs, source

@@ -1929,7 +1929,7 @@
Q1065966: Isomorphism theorem (φ : G →* H) :
G ⧸ φ.ker ≃* ↥φ.range
-

docs, source

+

docs, source

noncomputable def QuotientGroup.quotientInfEquivProdNormalQuotient @@ -1941,7 +1941,7 @@
Q1065966: Isomorphism theorem [N.Normal] :
↥H ⧸ N.subgroupOf H ≃* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
-

docs, source

+

docs, source

def QuotientGroup.quotientQuotientEquivQuotient @@ -1959,7 +1959,7 @@
Q1065966: Isomorphism theorem (h : N ≤ M) :
(G ⧸ N) ⧸ Subgroup.map (QuotientGroup.mk' N) M ≃* G ⧸ M
-

docs, source

+

docs, source

@@ -1996,7 +1996,7 @@
Q1067156: Dominated convergence (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => F n a) Filter.atTop (nhds (f a))) :
Filter.Tendsto (fun (n : ℕ) => ∫ (a : α), F n a ∂μ) Filter.atTop (nhds (∫ (a : α), f a ∂μ))
-

docs, source

+

docs, source

@@ -2027,7 +2027,7 @@
Q1067156X: Bounded convergence (fs_lim : ∀ (ω : Ω), Filter.Tendsto (fun (n : ℕ) => (fs n) ω) Filter.atTop (nhds (f ω))) :
Filter.Tendsto (fun (n : ℕ) => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) Filter.atTop (nhds (∫⁻ (ω : Ω), ↑(f ω) ∂↑μ))
-

docs, source

+

docs, source

theorem MeasureTheory.tendsto_lintegral_nn_filter_of_le_const @@ -2059,7 +2059,7 @@
Q1067156X: Bounded convergence (fs_lim : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (i : ι) => (fs i) ω) L (nhds (f ω))) :
Filter.Tendsto (fun (i : ι) => ∫⁻ (ω : Ω), ↑((fs i) ω) ∂μ) L (nhds (∫⁻ (ω : Ω), ↑(f ω) ∂μ))
-

docs, source

+

docs, source

@@ -2094,7 +2094,7 @@
Q1068085: Closed graph theorem < (hg : IsClosed ↑g.graph) :
Continuous ⇑g
-

docs, source

+

docs, source

@@ -2120,7 +2120,7 @@
Q1068283: Löwenheim–Skolem th (h2 : Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ) :
∃ (N : CategoryTheory.Bundled L.Structure), (Nonempty (L.ElementaryEmbedding (↑N) M) ∨ Nonempty (L.ElementaryEmbedding M ↑N)) ∧ Cardinal.mk ↑N = κ
-

docs, source

+

docs, source

@@ -2143,7 +2143,7 @@
Q1068976: Hilbert's Nullstellens (I : Ideal (MvPolynomial σ k)) :
MvPolynomial.vanishingIdeal (MvPolynomial.zeroLocus I) = I.radical
-

docs, source

+

docs, source

@@ -2156,7 +2156,7 @@
Q1082910: Euler's partition theo Theorems100.partition_theorem (n : ℕ) :
(Nat.Partition.odds n).card = (Nat.Partition.distincts n).card
-

docs, source

+

docs, source

@@ -2197,7 +2197,7 @@
Q1097021: Minkowski's theorem (h : μ F * 2 ^ Module.finrank ℝ E < μ s) :
∃ (x : ↥L), x ≠ 0 ∧ ↑x ∈ s
-

docs, source

+

docs, source

@@ -2216,7 +2216,7 @@
Q1137014: Tychonoff's theorem {s : (i : ι) → Set (X i)} :
(∀ (i : ι), IsCompact (s i)) → IsCompact {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i}
-

docs, source

+

docs, source

@@ -2240,7 +2240,7 @@
Q1137206: Taylor's theorem (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo 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) / ↑(n + 1).factorial
-

docs, source

+

docs, source

theorem taylor_mean_remainder_cauchy @@ -2257,7 +2257,7 @@
Q1137206: Taylor's theorem (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo 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 / ↑n.factorial * (x - x₀)
-

docs, source

+

docs, source

@@ -2280,7 +2280,7 @@
Q1139041: Cauchy's theorem (hdvd : p ∣ Fintype.card G) :
∃ (x : G), orderOf x = p
-

docs, source

+

docs, source

@@ -2324,7 +2324,7 @@
Q1149022: Fubini's theorem (hf : MeasureTheory.Integrable f (μ.prod ν)) :
∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
-

docs, source

+

docs, source

@@ -2339,7 +2339,7 @@
Q1149458: Compactness theorem {T : L.Theory} :
T.IsSatisfiable ↔ T.IsFinitelySatisfiable
-

docs, source

+

docs, source

@@ -2368,7 +2368,7 @@
Q1153584: Monotone convergence t (h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (F x))) :
Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), f n x ∂μ) Filter.atTop (nhds (∫ (x : α), F x ∂μ))
-

docs, source

+

docs, source

theorem MeasureTheory.lintegral_tendsto_of_tendsto_of_monotone @@ -2388,7 +2388,7 @@
Q1153584: Monotone convergence t (h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (F x))) :
Filter.Tendsto (fun (n : ℕ) => ∫⁻ (x : α), f n x ∂μ) Filter.atTop (nhds (∫⁻ (x : α), F x ∂μ))
-

docs, source

+

docs, source

@@ -2409,7 +2409,7 @@
Q1186808: Lucas's theorem (ha₂ : k < p ^ a) :
↑(n.choose k) ≡ ∏ i ∈ Finset.range a, ↑((n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]
-

docs, source

+

docs, source

@@ -2430,7 +2430,7 @@
Q1187646: Fundamental theorem on (φ : G →* H) :
G ⧸ φ.ker ≃* ↥φ.range
-

docs, source

+

docs, source

@@ -2441,7 +2441,7 @@
Q1188392: Zeckendorf's theorem <
def Nat.zeckendorfEquiv :
ℕ ≃ { l : List ℕ // l.IsZeckendorfRep }
-

docs, source

+

docs, source

@@ -2460,7 +2460,7 @@
Q1191319: Radon–Nikodym theore [μ.HaveLebesgueDecomposition ν] :
μ.AbsolutelyContinuous ν ↔ ν.withDensity (μ.rnDeriv ν) = μ
-

docs, source

+

docs, source

@@ -2509,7 +2509,7 @@
Q1191709: Egorov's theorem (hε : 0 < ε) :
∃ t ⊆ s, MeasurableSet t ∧ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g Filter.atTop (s \ t)
-

docs, source

+

docs, source

@@ -2528,7 +2528,7 @@
Q1194053: Metrization theorems < [SecondCountableTopology X] :
TopologicalSpace.MetrizableSpace X
-

docs, source

+

docs, source

Urysohn's metrization theorem (only)

@@ -2559,7 +2559,7 @@
Q1217677: Fundamental theorem of (hb : Filter.Tendsto f (nhds b ⊓ MeasureTheory.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 @@ -2583,7 +2583,7 @@
Q1217677: Fundamental theorem of (f'int : IntervalIntegrable f' MeasureTheory.volume a b) :
∫ (y : ℝ) in a..b, f' y = f b - f a
-

docs, source

+

docs, source

@@ -2604,7 +2604,7 @@
Q1243340: Birkhoff–Von Neumann [LinearOrderedField R] :
↑(doublyStochastic R n) = (convexHull R) {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}
-

docs, source

+

docs, source

@@ -2623,7 +2623,7 @@
Q1259814: Nielsen–Schreier the (H : Subgroup G) :
IsFreeGroup ↥H
-

docs, source

+

docs, source

@@ -2661,7 +2661,7 @@
Q1306095: Whitney embedding theo [CompactSpace M] :
∃ (n : ℕ) (e : M → EuclideanSpace ℝ (Fin n)), ContMDiff I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (↑⊤) e ∧ Topology.IsClosedEmbedding e ∧ ∀ (x : M), Function.Injective ⇑(mfderiv I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) e x)
-

docs, source

+

docs, source

baby version: for compact manifolds; embedding into some n

@@ -2688,7 +2688,7 @@
Q1346677: Tietze extension theor (he : Topology.IsClosedEmbedding e) :
∃ (g : BoundedContinuousFunction Y ℝ), ‖g‖ = ‖f‖ ∧ ⇑g ∘ e = ⇑f
-

docs, source

+

docs, source

@@ -2731,7 +2731,7 @@
Q1426292: Banach–Steinhaus the (h : ∀ (x : E), ∃ (C : ℝ), ∀ (i : ι), ‖(g i) x‖ ≤ C) :
∃ (C' : ℝ), ∀ (i : ι), ‖g i‖ ≤ C'
-

docs, source

+

docs, source

@@ -2764,7 +2764,7 @@
Q1477053: Arzelà–Ascoli theor (H : Equicontinuous fun (x : ↑A) => ⇑↑x) :
IsCompact (closure A)
-

docs, source

+

docs, source

@@ -2777,7 +2777,7 @@
Q1506253: Euclid's theorem Nat.exists_infinite_primes (n : ℕ) :
∃ (p : ℕ), n ≤ p ∧ Nat.Prime p
-

docs, source

+

docs, source

@@ -2790,7 +2790,7 @@
Q1542114: Bézout's theorem Nat.gcd_eq_gcd_ab (x y : ℕ) :
↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y
-

docs, source

+

docs, source

@@ -2813,7 +2813,7 @@
Q1566341: Hindman's theorem (scov : Hindman.FP a ⊆ ⋃₀ s) :
∃ c ∈ s, ∃ (b : Stream' M), Hindman.FP b ⊆ c
-

docs, source

+

docs, source

@@ -2831,7 +2831,7 @@
Q1568811: Hahn decomposition the (s : MeasureTheory.SignedMeasure α) :
∃ (i : Set α) (j : Set α), MeasurableSet i ∧ MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i ∧ MeasurableSet j ∧ MeasureTheory.VectorMeasure.restrict s j ≤ MeasureTheory.VectorMeasure.restrict 0 j ∧ IsCompl i j
-

docs, source

+

docs, source

@@ -2866,7 +2866,7 @@
Q1632433: Helly's theorem (h_inter : ∀ I ⊆ s, I.card = Module.finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) :
(⋂ i ∈ s, F i).Nonempty
-

docs, source

+

docs, source

@@ -2881,7 +2881,7 @@
Q1687147: Sprague–Grundy theor [G.Impartial] :
G ≈ SetTheory.PGame.nim (Nimber.toOrdinal G.grundyValue)
-

docs, source

+

docs, source

@@ -2903,7 +2903,7 @@
Q1752621: Sylvester's law of ine (Q : QuadraticForm ℝ M) :
∃ (w : Fin (Module.finrank ℝ M) → ℝ), (∀ (i : Fin (Module.finrank ℝ M)), w i = -1 ∨ w i = 0 ∨ w i = 1) ∧ QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℝ w)
-

docs, source

+

docs, source

@@ -2936,7 +2936,7 @@
Q1816952: Schur's lemma [FiniteDimensional 𝕜 (X ⟶ X)] :
Module.finrank 𝕜 (X ⟶ X) = 1
-

docs, source

+

docs, source

@@ -2959,7 +2959,7 @@
Q1893717: Rice's theorem (fC : f ∈ C) :
g ∈ C
-

docs, source

+

docs, source

@@ -2991,7 +2991,7 @@
Q2027347: Optional stopping theo τ ≤ π → (∃ (N : ℕ), ∀ (x : Ω), π x ≤ N) → ∫ (x : Ω), MeasureTheory.stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), MeasureTheory.stoppedValue f π x ∂μ -

docs, source

+

docs, source

@@ -3016,7 +3016,7 @@
Q2093886: Primitive element theo [Algebra.IsSeparable F E] :
∃ (α : E), F⟮α⟯ = ⊤
-

docs, source

+

docs, source

@@ -3035,7 +3035,7 @@
Q2226786: Sperner's theorem (h𝒜 : IsAntichain (fun (x1 x2 : Finset α) => x1 ⊆ x2) ↑𝒜) :
𝒜.card ≤ (Fintype.card α).choose (Fintype.card α / 2)
-

docs, source

+

docs, source

@@ -3056,7 +3056,7 @@
Q2226800: Schur–Zassenhaus the (hN : (Nat.card ↥N).Coprime N.index) :
∃ (H : Subgroup G), H.IsComplement' N
-

docs, source

+

docs, source

@@ -3076,7 +3076,7 @@
Q2253746: Bertrand's ballot theo Ballot.ballot_problem (q p : ℕ) :
q < p → (ProbabilityTheory.uniformOn (Ballot.countedSequence p q)) Ballot.staysPositive = (↑p - ↑q) / (↑p + ↑q)
-

docs, source

+

docs, source

@@ -3109,7 +3109,7 @@
Q2275191: Lebesgue differentiati (h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤) :
∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (a : Set α) => (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (nhds (f x))
-

docs, source

+

docs, source

@@ -3132,7 +3132,7 @@
Q2471737: Carathéodory's theore {s : Set E} :
(convexHull 𝕜) s = ⋃ (t : Finset E), ⋃ (_ : ↑t ⊆ s), ⋃ (_ : AffineIndependent 𝕜 Subtype.val), (convexHull 𝕜) ↑t
-

docs, source

+

docs, source

@@ -3155,7 +3155,7 @@
Q2525646: Jordan–Hölder theor (ht : RelSeries.last s₁ = RelSeries.last s₂) :
s₁.Equivalent s₂
-

docs, source

+

docs, source

@@ -3170,7 +3170,7 @@
Q2919401: Ostrowski's theorem (hf_nontriv : f.IsNontrivial) :
f ≈ Rat.AbsoluteValue.real ∨ ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f ≈ Rat.AbsoluteValue.padic p
-

docs, source

+

docs, source

@@ -3219,7 +3219,7 @@
Q3229352: Vitali covering theore (hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x) :
∃ u ⊆ t, u.Countable ∧ u.PairwiseDisjoint B ∧ μ (s \ ⋃ a ∈ u, B a) = 0
-

docs, source

+

docs, source

@@ -3247,7 +3247,7 @@
Q3527102: Kruskal–Katona theor (h𝒞 : Finset.Colex.IsInitSeg 𝒞 r) :
𝒞.shadow.card ≤ 𝒜.shadow.card
-

docs, source

+

docs, source

@@ -3274,7 +3274,7 @@
Q3527118: Mahler's theorem (f : C(ℤ_[p], E)) :
HasSum (fun (n : ℕ) => PadicInt.mahlerTerm ((fwdDiff 1)^[n] (⇑f) 0) n) f
-

docs, source

+

docs, source

@@ -3299,7 +3299,7 @@
Q3527189: Lattice theorem (h : N ≤ M) :
(G ⧸ N) ⧸ Subgroup.map (QuotientGroup.mk' N) M ≃* G ⧸ M
-

docs, source

+

docs, source

@@ -3330,7 +3330,7 @@
Q3527205: Dimension theorem for (v' : Basis ι' R M) :
Cardinal.lift.{w', w} (Cardinal.mk ι) = Cardinal.lift.{w, w'} (Cardinal.mk ι')
-

docs, source

+

docs, source

@@ -3357,7 +3357,7 @@
Q3527215: Hilbert projection the (u : F) :
∃ v ∈ K, ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
-

docs, source

+

docs, source

@@ -3384,7 +3384,7 @@
Q3527250: Hadamard three-lines t (hB : BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)) :
‖f z‖ ≤ ‖Complex.HadamardThreeLines.interpStrip f z‖
-

docs, source

+

docs, source

@@ -3403,7 +3403,7 @@
Q3527263: Kleene fixed-point the (h : OmegaCompletePartialOrder.ωScottContinuous ⇑f) :
OrderHom.lfp f = ⨆ (n : ℕ), (⇑f)^[n] ⊥
-

docs, source

+

docs, source

@@ -3442,7 +3442,7 @@
Q3984053: Fourier inversion theo (h'f : MeasureTheory.Integrable (Real.fourierIntegral f) MeasureTheory.volume) :
Real.fourierIntegralInv (Real.fourierIntegral f) = f
-

docs, source

+

docs, source

@@ -3481,7 +3481,7 @@
Q4378868: Phragmén–Lindelöf (hzb : z.im ≤ b) :
‖f z‖ ≤ C
-

docs, source

+

docs, source

@@ -3518,7 +3518,7 @@
Q4695203: Four functions theorem (s t : Finset α) :
(∑ a ∈ s, f₁ a) * ∑ a ∈ t, f₂ a ≤ (∑ a ∈ s ⊼ t, f₃ a) * ∑ a ∈ s ⊻ t, f₄ a
-

docs, source

+

docs, source

@@ -3546,7 +3546,7 @@
Q4830725: Ax–Grothendieck theo Set.MapsTo (fun (v : ι → K) (i : ι) => (MvPolynomial.eval v) (p i)) S S → Set.InjOn (fun (v : ι → K) (i : ι) => (MvPolynomial.eval v) (p i)) S → Set.SurjOn (fun (v : ι → K) (i : ι) => (MvPolynomial.eval v) (p i)) S S -

docs, source

+

docs, source

@@ -3571,7 +3571,7 @@
Q5171652: Corners theorem (hAε : ε * ↑n ^ 2 ≤ ↑A.card) :
¬IsCornerFree ↑A
-

docs, source

+

docs, source

@@ -3592,7 +3592,7 @@
Q5437947: Fatou–Lebesgue theor (h_meas : ∀ (n : ℕ), Measurable (f n)) :
∫⁻ (a : α), Filter.liminf (fun (n : ℕ) => f n a) Filter.atTop ∂μ ≤ Filter.liminf (fun (n : ℕ) => ∫⁻ (a : α), f n a ∂μ) Filter.atTop
-

docs, source

+

docs, source

@@ -3613,7 +3613,7 @@
Q5504427: Friendship theorem [Nonempty V] :
Theorems100.ExistsPolitician G
-

docs, source

+

docs, source

@@ -3653,7 +3653,7 @@
Q6813106: Mellin inversion theor (hfx : ContinuousAt f x) :
mellinInv σ (mellin f) x = f x
-

docs, source

+

docs, source

@@ -3680,7 +3680,7 @@
Q7432915: Schroeder–Bernstein (hg : MeasurableEmbedding g) :
α ≃ᵐ β
-

docs, source

+

docs, source

@@ -3707,7 +3707,7 @@
Q7433182: Schwartz–Zippel theo (S : Fin n → Finset R) :
↑(Finset.filter (fun (x : Fin n → R) => (MvPolynomial.eval x) p = 0) (Fintype.piFinset fun (i : Fin n) => S i)).card / ∏ i : Fin n, ↑(S i).card ≤ p.support.sup fun (s : Fin n →₀ ℕ) => ∑ i : Fin n, ↑(s i) / ↑(S i).card
-

docs, source

+

docs, source

@@ -3736,7 +3736,7 @@
Q7820874: Tonelli's theorem (hf : AEMeasurable f (μ.prod ν)) :
∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
-

docs, source

+

docs, source

@@ -3764,7 +3764,7 @@
Q7888360: Structure theorem for [h' : Module.Finite R N] :
∃ (n : ℕ) (ι : Type u) (x : Fintype ι) (p : ι → R) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ), Nonempty (N ≃ₗ[R] (Fin n →₀ R) × DirectSum ι fun (i : ι) => R ⧸ Submodule.span R {p i ^ e i})
-

docs, source

+

docs, source

@@ -3794,7 +3794,7 @@
Q9993851: Lax–Milgram theorem (coercive : IsCoercive B) :
V ≃L[ℝ] V
-

docs, source

+

docs, source

@@ -3829,7 +3829,7 @@
Q11352023: Vitali convergence t (hg : MeasureTheory.Memℒp g p μ) :
MeasureTheory.TendstoInMeasure μ f Filter.atTop g ∧ MeasureTheory.UnifIntegrable f p μ ∧ MeasureTheory.UnifTight f p μ ↔ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0)
-

docs, source

+

docs, source

@@ -3843,7 +3843,7 @@
Q16251580: Matiyasevich's theor {a k x y : ℕ} :
(∃ (a1 : 1 < a), Pell.xn a1 k = x ∧ Pell.yn a1 k = y) ↔ 1 < a ∧ k ≤ y ∧ (x = 1 ∧ y = 0 ∨ ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ), x * x - (a * a - 1) * y * y = 1 ∧ u * u - (a * a - 1) * v * v = 1 ∧ s * s - (b * b - 1) * t * t = 1 ∧ 1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])
-

docs, source

+

docs, source

@@ -3862,7 +3862,7 @@
Q17005116: Birkhoff's represent [DecidablePred SupIrred] :
LatticeHom α (Set { a : α // SupIrred a })
-

docs, source

+

docs, source

@@ -3879,7 +3879,7 @@
Q18206266: Euclid–Euler theor (perf : n.Perfect) :
∃ (k : ℕ), Nat.Prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1)
-

docs, source

+

docs, source

@@ -3890,7 +3890,7 @@
Q22952648: Uncountability of th
theorem Cardinal.not_countable_real :
¬Set.univ.Countable
-

docs, source

+

docs, source

diff --git a/lean_projects.html b/lean_projects.html index 11d4a3926..a50cb6f15 100644 --- a/lean_projects.html +++ b/lean_projects.html @@ -241,19 +241,25 @@
maintained by
-
con-nf
+
lftcm2020
maintained by - @YaelDillies + @jcommelin - @zeramorphic + @PatrickMassot
-

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 repository contains tutorials about Lean and mathlib that were developed +for the workshop Lean for the Curious Mathematician, +held in July 2020. The tutorials range from introductory lessons on numbers, +logic, and sets to advanced lessons on category theory and manifolds. +In addition to the materials found in this repository, we recommend watching +the videos +of the tutorials and lectures from the workshop.

- View on GitHub (★ 66) + View on GitHub (★ 66)
@@ -261,25 +267,19 @@
maintained by
-
lftcm2020
+
con-nf
maintained by - @jcommelin + @YaelDillies - @PatrickMassot + @zeramorphic
-

This repository contains tutorials about Lean and mathlib that were developed -for the workshop Lean for the Curious Mathematician, -held in July 2020. The tutorials range from introductory lessons on numbers, -logic, and sets to advanced lessons on category theory and manifolds. -In addition to the materials found in this repository, we recommend watching -the videos -of the tutorials and lectures from the workshop.

+

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 (★ 65) + View on GitHub (★ 66)
diff --git a/mathlib_stats.html b/mathlib_stats.html index d085142c2..d876d81bd 100644 --- a/mathlib_stats.html +++ b/mathlib_stats.html @@ -60,8 +60,8 @@

Counts

Contributors - 94441 - 180970 + 94483 + 181042 384 diff --git a/meet.html b/meet.html index 86d84ac47..2d6bd0501 100644 --- a/meet.html +++ b/meet.html @@ -310,18 +310,6 @@
Contributing
marker_right.bindPopup("Aaron Hill
GitHub: a-aronh"); markers.addLayer(marker_right); -var marker = L.marker([43.8563, 18.4131]); -marker.bindPopup("Atif Degirmendzic"); -markers.addLayer(marker); - -var marker_left = L.marker([43.8563, -341.5869]); -marker_left.bindPopup("Atif Degirmendzic"); -markers.addLayer(marker_left); - -var marker_right = L.marker([43.8563, 378.4131]); -marker_right.bindPopup("Atif Degirmendzic"); -markers.addLayer(marker_right); - var marker = L.marker([53.550556, 9.993333]); marker.bindPopup("Ekebonke"); markers.addLayer(marker); @@ -346,30 +334,6 @@
Contributing
marker_right.bindPopup("Wen Yang
GitHub: shuxuezhuyi"); markers.addLayer(marker_right); -var marker = L.marker([41.852507, 12.603816]); -marker.bindPopup("Rafael Leon Greenblatt
GitHub: RafaelGreenblatt"); -markers.addLayer(marker); - -var marker_left = L.marker([41.852507, -347.396184]); -marker_left.bindPopup("Rafael Leon Greenblatt
GitHub: RafaelGreenblatt"); -markers.addLayer(marker_left); - -var marker_right = L.marker([41.852507, 372.603816]); -marker_right.bindPopup("Rafael Leon Greenblatt
GitHub: RafaelGreenblatt"); -markers.addLayer(marker_right); - -var marker = L.marker([51.05011, -114.08529]); -marker.bindPopup("Hal Heinrich
GitHub: halheinrich"); -markers.addLayer(marker); - -var marker_left = L.marker([51.05011, -474.08529]); -marker_left.bindPopup("Hal Heinrich
GitHub: halheinrich"); -markers.addLayer(marker_left); - -var marker_right = L.marker([51.05011, 245.91471]); -marker_right.bindPopup("Hal Heinrich
GitHub: halheinrich"); -markers.addLayer(marker_right); - var marker = L.marker([52.3422, 5.6367]); marker.bindPopup("Josha Dekker
GitHub: JADekker"); markers.addLayer(marker); @@ -382,18 +346,6 @@
Contributing
marker_right.bindPopup("Josha Dekker
GitHub: JADekker"); markers.addLayer(marker_right); -var marker = L.marker([42.36, -71.06]); -marker.bindPopup("Michael P Touloumtzis
GitHub: mptz"); -markers.addLayer(marker); - -var marker_left = L.marker([42.36, -431.06]); -marker_left.bindPopup("Michael P Touloumtzis
GitHub: mptz"); -markers.addLayer(marker_left); - -var marker_right = L.marker([42.36, 288.94]); -marker_right.bindPopup("Michael P Touloumtzis
GitHub: mptz"); -markers.addLayer(marker_right); - var marker = L.marker([52.087216, 5.165171]); marker.bindPopup("Edward van de Meent
GitHub: blizzard_inc"); markers.addLayer(marker); @@ -466,18 +418,6 @@
Contributing
marker_right.bindPopup("Dhyan Aranha"); markers.addLayer(marker_right); -var marker = L.marker([42.450528451924626, -76.48143612664352]); -marker.bindPopup("Samuel Homiller
GitHub: shomiller"); -markers.addLayer(marker); - -var marker_left = L.marker([42.450528451924626, -436.48143612664353]); -marker_left.bindPopup("Samuel Homiller
GitHub: shomiller"); -markers.addLayer(marker_left); - -var marker_right = L.marker([42.450528451924626, 283.51856387335647]); -marker_right.bindPopup("Samuel Homiller
GitHub: shomiller"); -markers.addLayer(marker_right); - var marker = L.marker([39.33033, -76.614983]); marker.bindPopup("Daniel Carranza
GitHub: daniel-carranza"); markers.addLayer(marker); @@ -490,40 +430,28 @@
Contributing
marker_right.bindPopup("Daniel Carranza
GitHub: daniel-carranza"); markers.addLayer(marker_right); -var marker = L.marker([45.48036798292276, -122.62853119691442]); -marker.bindPopup("Tristan Figueroa-Reid
GitHub: LeoDog896"); -markers.addLayer(marker); - -var marker_left = L.marker([45.48036798292276, -482.6285311969144]); -marker_left.bindPopup("Tristan Figueroa-Reid
GitHub: LeoDog896"); -markers.addLayer(marker_left); - -var marker_right = L.marker([45.48036798292276, 237.37146880308558]); -marker_right.bindPopup("Tristan Figueroa-Reid
GitHub: LeoDog896"); -markers.addLayer(marker_right); - -var marker = L.marker([-37.79813, 144.963769]); -marker.bindPopup("Moritz Doll
GitHub: mcdoll"); +var marker = L.marker([43.8563, 18.4131]); +marker.bindPopup("Atif Degirmendzic"); markers.addLayer(marker); -var marker_left = L.marker([-37.79813, -215.036231]); -marker_left.bindPopup("Moritz Doll
GitHub: mcdoll"); +var marker_left = L.marker([43.8563, -341.5869]); +marker_left.bindPopup("Atif Degirmendzic"); markers.addLayer(marker_left); -var marker_right = L.marker([-37.79813, 504.963769]); -marker_right.bindPopup("Moritz Doll
GitHub: mcdoll"); +var marker_right = L.marker([43.8563, 378.4131]); +marker_right.bindPopup("Atif Degirmendzic"); markers.addLayer(marker_right); -var marker = L.marker([38.9871, -77.21713]); -marker.bindPopup("Hunter Monroe
GitHub: hmonroe"); +var marker = L.marker([45.48036798292276, -122.62853119691442]); +marker.bindPopup("Tristan Figueroa-Reid
GitHub: LeoDog896"); markers.addLayer(marker); -var marker_left = L.marker([38.9871, -437.21713]); -marker_left.bindPopup("Hunter Monroe
GitHub: hmonroe"); +var marker_left = L.marker([45.48036798292276, -482.6285311969144]); +marker_left.bindPopup("Tristan Figueroa-Reid
GitHub: LeoDog896"); markers.addLayer(marker_left); -var marker_right = L.marker([38.9871, 282.78287]); -marker_right.bindPopup("Hunter Monroe
GitHub: hmonroe"); +var marker_right = L.marker([45.48036798292276, 237.37146880308558]); +marker_right.bindPopup("Tristan Figueroa-Reid
GitHub: LeoDog896"); markers.addLayer(marker_right); var marker = L.marker([48.138534, 11.576959]); @@ -550,16 +478,16 @@
Contributing
marker_right.bindPopup("Ashley Blacquiere
GitHub: ashandoak"); markers.addLayer(marker_right); -var marker = L.marker([37.55, -121.99]); -marker.bindPopup("Anirudh Rao
GitHub: rao107"); +var marker = L.marker([41.852507, 12.603816]); +marker.bindPopup("Rafael Leon Greenblatt
GitHub: RafaelGreenblatt"); markers.addLayer(marker); -var marker_left = L.marker([37.55, -481.99]); -marker_left.bindPopup("Anirudh Rao
GitHub: rao107"); +var marker_left = L.marker([41.852507, -347.396184]); +marker_left.bindPopup("Rafael Leon Greenblatt
GitHub: RafaelGreenblatt"); markers.addLayer(marker_left); -var marker_right = L.marker([37.55, 238.01]); -marker_right.bindPopup("Anirudh Rao
GitHub: rao107"); +var marker_right = L.marker([41.852507, 372.603816]); +marker_right.bindPopup("Rafael Leon Greenblatt
GitHub: RafaelGreenblatt"); markers.addLayer(marker_right); var marker = L.marker([37.7889, 122.3982]); @@ -598,40 +526,16 @@
Contributing
marker_right.bindPopup("Martin Harrison
GitHub: reamstack"); markers.addLayer(marker_right); -var marker = L.marker([36.00315447171814, -78.94226527274706]); -marker.bindPopup("Ricardo Prado Cunha
GitHub: MithicSpirit"); -markers.addLayer(marker); - -var marker_left = L.marker([36.00315447171814, -438.9422652727471]); -marker_left.bindPopup("Ricardo Prado Cunha
GitHub: MithicSpirit"); -markers.addLayer(marker_left); - -var marker_right = L.marker([36.00315447171814, 281.0577347272529]); -marker_right.bindPopup("Ricardo Prado Cunha
GitHub: MithicSpirit"); -markers.addLayer(marker_right); - -var marker = L.marker([39.7392, -104.9903]); -marker.bindPopup("Chance Nahuway
GitHub: chancenahuway"); -markers.addLayer(marker); - -var marker_left = L.marker([39.7392, -464.9903]); -marker_left.bindPopup("Chance Nahuway
GitHub: chancenahuway"); -markers.addLayer(marker_left); - -var marker_right = L.marker([39.7392, 255.0097]); -marker_right.bindPopup("Chance Nahuway
GitHub: chancenahuway"); -markers.addLayer(marker_right); - -var marker = L.marker([47.610609, -122.182161]); -marker.bindPopup("Jair Taylor"); +var marker = L.marker([51.05011, -114.08529]); +marker.bindPopup("Hal Heinrich
GitHub: halheinrich"); markers.addLayer(marker); -var marker_left = L.marker([47.610609, -482.182161]); -marker_left.bindPopup("Jair Taylor"); +var marker_left = L.marker([51.05011, -474.08529]); +marker_left.bindPopup("Hal Heinrich
GitHub: halheinrich"); markers.addLayer(marker_left); -var marker_right = L.marker([47.610609, 237.817839]); -marker_right.bindPopup("Jair Taylor"); +var marker_right = L.marker([51.05011, 245.91471]); +marker_right.bindPopup("Hal Heinrich
GitHub: halheinrich"); markers.addLayer(marker_right); var marker = L.marker([36.9957301, -122.0615848]); @@ -646,124 +550,148 @@
Contributing
marker_right.bindPopup("Kyle Miller
GitHub: kmill"); markers.addLayer(marker_right); -var marker = L.marker([35.503522, -80.83476]); -marker.bindPopup("Lars Ericson"); +var marker = L.marker([33.64401167447331, -117.84117044314782]); +marker.bindPopup("Tomas Ortega
GitHub: https://github.com/TomasOrtega"); markers.addLayer(marker); -var marker_left = L.marker([35.503522, -440.83476]); -marker_left.bindPopup("Lars Ericson"); +var marker_left = L.marker([33.64401167447331, -477.8411704431478]); +marker_left.bindPopup("Tomas Ortega
GitHub: https://github.com/TomasOrtega"); markers.addLayer(marker_left); -var marker_right = L.marker([35.503522, 279.16524]); -marker_right.bindPopup("Lars Ericson"); +var marker_right = L.marker([33.64401167447331, 242.1588295568522]); +marker_right.bindPopup("Tomas Ortega
GitHub: https://github.com/TomasOrtega"); markers.addLayer(marker_right); -var marker = L.marker([43.6532, -79.3832]); -marker.bindPopup("Avi Craimer
GitHub: AviCraimer"); +var marker = L.marker([39.52, -119.81]); +marker.bindPopup("Richard Kelley
GitHub: richardkelley"); markers.addLayer(marker); -var marker_left = L.marker([43.6532, -439.3832]); -marker_left.bindPopup("Avi Craimer
GitHub: AviCraimer"); +var marker_left = L.marker([39.52, -479.81]); +marker_left.bindPopup("Richard Kelley
GitHub: richardkelley"); markers.addLayer(marker_left); -var marker_right = L.marker([43.6532, 280.6168]); -marker_right.bindPopup("Avi Craimer
GitHub: AviCraimer"); +var marker_right = L.marker([39.52, 240.19]); +marker_right.bindPopup("Richard Kelley
GitHub: richardkelley"); markers.addLayer(marker_right); -var marker = L.marker([-16.434067, -51.112691]); -marker.bindPopup("Fabrício S. Paranhos"); +var marker = L.marker([42.36, -71.06]); +marker.bindPopup("Michael P Touloumtzis
GitHub: mptz"); markers.addLayer(marker); -var marker_left = L.marker([-16.434067, -411.112691]); -marker_left.bindPopup("Fabrício S. Paranhos"); +var marker_left = L.marker([42.36, -431.06]); +marker_left.bindPopup("Michael P Touloumtzis
GitHub: mptz"); markers.addLayer(marker_left); -var marker_right = L.marker([-16.434067, 308.887309]); -marker_right.bindPopup("Fabrício S. Paranhos"); +var marker_right = L.marker([42.36, 288.94]); +marker_right.bindPopup("Michael P Touloumtzis
GitHub: mptz"); markers.addLayer(marker_right); -var marker = L.marker([33.64401167447331, -117.84117044314782]); -marker.bindPopup("Tomas Ortega
GitHub: https://github.com/TomasOrtega"); +var marker = L.marker([33.99825, -81.02549]); +marker.bindPopup("Matthew Ballard
GitHub: mattrobball"); markers.addLayer(marker); -var marker_left = L.marker([33.64401167447331, -477.8411704431478]); -marker_left.bindPopup("Tomas Ortega
GitHub: https://github.com/TomasOrtega"); +var marker_left = L.marker([33.99825, -441.02549]); +marker_left.bindPopup("Matthew Ballard
GitHub: mattrobball"); markers.addLayer(marker_left); -var marker_right = L.marker([33.64401167447331, 242.1588295568522]); -marker_right.bindPopup("Tomas Ortega
GitHub: https://github.com/TomasOrtega"); +var marker_right = L.marker([33.99825, 278.97451]); +marker_right.bindPopup("Matthew Ballard
GitHub: mattrobball"); markers.addLayer(marker_right); -var marker = L.marker([12.9716, 77.5946]); -marker.bindPopup("Mrigank Pawagi
GitHub: mrigankpawagi"); +var marker = L.marker([38.794013, -89.999591]); +marker.bindPopup("Jireh Loreaux
GitHub: j-loreaux"); markers.addLayer(marker); -var marker_left = L.marker([12.9716, -282.4054]); -marker_left.bindPopup("Mrigank Pawagi
GitHub: mrigankpawagi"); +var marker_left = L.marker([38.794013, -449.999591]); +marker_left.bindPopup("Jireh Loreaux
GitHub: j-loreaux"); markers.addLayer(marker_left); -var marker_right = L.marker([12.9716, 437.5946]); -marker_right.bindPopup("Mrigank Pawagi
GitHub: mrigankpawagi"); +var marker_right = L.marker([38.794013, 270.000409]); +marker_right.bindPopup("Jireh Loreaux
GitHub: j-loreaux"); markers.addLayer(marker_right); -var marker = L.marker([-22.9, -43.17]); -marker.bindPopup("Henrique Coelho"); +var marker = L.marker([48.119134, -1.641871]); +marker.bindPopup("Sébastien Gouëzel
GitHub: sgouezel"); markers.addLayer(marker); -var marker_left = L.marker([-22.9, -403.17]); -marker_left.bindPopup("Henrique Coelho"); +var marker_left = L.marker([48.119134, -361.641871]); +marker_left.bindPopup("Sébastien Gouëzel
GitHub: sgouezel"); markers.addLayer(marker_left); -var marker_right = L.marker([-22.9, 316.83]); -marker_right.bindPopup("Henrique Coelho"); +var marker_right = L.marker([48.119134, 358.358129]); +marker_right.bindPopup("Sébastien Gouëzel
GitHub: sgouezel"); markers.addLayer(marker_right); -var marker = L.marker([-35.2813, 149.1183]); -marker.bindPopup("Dom Verity
GitHub: dom-verity@github.com"); +var marker = L.marker([34.069364114046024, -118.44351443013207]); +marker.bindPopup("Aaron Anderson
GitHub: awainverse"); markers.addLayer(marker); -var marker_left = L.marker([-35.2813, -210.8817]); -marker_left.bindPopup("Dom Verity
GitHub: dom-verity@github.com"); +var marker_left = L.marker([34.069364114046024, -478.44351443013204]); +marker_left.bindPopup("Aaron Anderson
GitHub: awainverse"); markers.addLayer(marker_left); -var marker_right = L.marker([-35.2813, 509.1183]); -marker_right.bindPopup("Dom Verity
GitHub: dom-verity@github.com"); +var marker_right = L.marker([34.069364114046024, 241.55648556986793]); +marker_right.bindPopup("Aaron Anderson
GitHub: awainverse"); markers.addLayer(marker_right); -var marker = L.marker([20.173226, 85.684102]); -marker.bindPopup("Abhijit Chakraborty
GitHub: Abhijit-niser"); +var marker = L.marker([48.198854, 16.367016]); +marker.bindPopup("Stefan Hetzl
GitHub: shetzl"); markers.addLayer(marker); -var marker_left = L.marker([20.173226, -274.315898]); -marker_left.bindPopup("Abhijit Chakraborty
GitHub: Abhijit-niser"); +var marker_left = L.marker([48.198854, -343.632984]); +marker_left.bindPopup("Stefan Hetzl
GitHub: shetzl"); markers.addLayer(marker_left); -var marker_right = L.marker([20.173226, 445.684102]); -marker_right.bindPopup("Abhijit Chakraborty
GitHub: Abhijit-niser"); +var marker_right = L.marker([48.198854, 376.367016]); +marker_right.bindPopup("Stefan Hetzl
GitHub: shetzl"); markers.addLayer(marker_right); -var marker = L.marker([1.295065068415129, 103.77486870277362]); -marker.bindPopup("Ilya Sergey
GitHub: ilyasergey"); +var marker = L.marker([52.334811, 4.864481]); +marker.bindPopup("Sander Dahmen"); markers.addLayer(marker); -var marker_left = L.marker([1.295065068415129, -256.22513129722637]); -marker_left.bindPopup("Ilya Sergey
GitHub: ilyasergey"); +var marker_left = L.marker([52.334811, -355.135519]); +marker_left.bindPopup("Sander Dahmen"); markers.addLayer(marker_left); -var marker_right = L.marker([1.295065068415129, 463.77486870277363]); -marker_right.bindPopup("Ilya Sergey
GitHub: ilyasergey"); +var marker_right = L.marker([52.334811, 364.864481]); +marker_right.bindPopup("Sander Dahmen"); markers.addLayer(marker_right); -var marker = L.marker([39.52, -119.81]); -marker.bindPopup("Richard Kelley
GitHub: richardkelley"); +var marker = L.marker([32.0717, 34.8469]); +marker.bindPopup("Daniel Weber
GitHub: Command-Master"); markers.addLayer(marker); -var marker_left = L.marker([39.52, -479.81]); -marker_left.bindPopup("Richard Kelley
GitHub: richardkelley"); +var marker_left = L.marker([32.0717, -325.1531]); +marker_left.bindPopup("Daniel Weber
GitHub: Command-Master"); markers.addLayer(marker_left); -var marker_right = L.marker([39.52, 240.19]); -marker_right.bindPopup("Richard Kelley
GitHub: richardkelley"); +var marker_right = L.marker([32.0717, 394.8469]); +marker_right.bindPopup("Daniel Weber
GitHub: Command-Master"); +markers.addLayer(marker_right); + +var marker = L.marker([41.715137, 44.827095]); +marker.bindPopup("Evgenia Karunus
GitHub: lakesare"); +markers.addLayer(marker); + +var marker_left = L.marker([41.715137, -315.172905]); +marker_left.bindPopup("Evgenia Karunus
GitHub: lakesare"); +markers.addLayer(marker_left); + +var marker_right = L.marker([41.715137, 404.827095]); +marker_right.bindPopup("Evgenia Karunus
GitHub: lakesare"); +markers.addLayer(marker_right); + +var marker = L.marker([42.450528451924626, -76.48143612664352]); +marker.bindPopup("Samuel Homiller
GitHub: shomiller"); +markers.addLayer(marker); + +var marker_left = L.marker([42.450528451924626, -436.48143612664353]); +marker_left.bindPopup("Samuel Homiller
GitHub: shomiller"); +markers.addLayer(marker_left); + +var marker_right = L.marker([42.450528451924626, 283.51856387335647]); +marker_right.bindPopup("Samuel Homiller
GitHub: shomiller"); markers.addLayer(marker_right); var marker = L.marker([43.56, -79.63]); @@ -778,184 +706,412 @@
Contributing
marker_right.bindPopup("Frederick Pu
GitHub: FrederickPu"); markers.addLayer(marker_right); -var marker = L.marker([39.22264454871392, 9.114527859227785]); -marker.bindPopup("Federico Dal Pio Luogo
GitHub: dalps"); +var marker = L.marker([43.6532, 79.3832]); +marker.bindPopup("Matthew Bolan
GitHub: mjtb49"); markers.addLayer(marker); -var marker_left = L.marker([39.22264454871392, -350.8854721407722]); -marker_left.bindPopup("Federico Dal Pio Luogo
GitHub: dalps"); +var marker_left = L.marker([43.6532, -280.6168]); +marker_left.bindPopup("Matthew Bolan
GitHub: mjtb49"); markers.addLayer(marker_left); -var marker_right = L.marker([39.22264454871392, 369.1145278592278]); -marker_right.bindPopup("Federico Dal Pio Luogo
GitHub: dalps"); +var marker_right = L.marker([43.6532, 439.3832]); +marker_right.bindPopup("Matthew Bolan
GitHub: mjtb49"); markers.addLayer(marker_right); -var marker = L.marker([53.568059, 9.974478]); -marker.bindPopup("Roman Stehling"); +var marker = L.marker([-37.79813, 144.963769]); +marker.bindPopup("Moritz Doll
GitHub: mcdoll"); markers.addLayer(marker); -var marker_left = L.marker([53.568059, -350.025522]); -marker_left.bindPopup("Roman Stehling"); +var marker_left = L.marker([-37.79813, -215.036231]); +marker_left.bindPopup("Moritz Doll
GitHub: mcdoll"); markers.addLayer(marker_left); -var marker_right = L.marker([53.568059, 369.974478]); -marker_right.bindPopup("Roman Stehling"); +var marker_right = L.marker([-37.79813, 504.963769]); +marker_right.bindPopup("Moritz Doll
GitHub: mcdoll"); markers.addLayer(marker_right); -var marker = L.marker([33.99825, -81.02549]); -marker.bindPopup("Matthew Ballard
GitHub: mattrobball"); +var marker = L.marker([52.19835, 0.12053]); +marker.bindPopup("Eric Wieser
GitHub: eric-wieser"); markers.addLayer(marker); -var marker_left = L.marker([33.99825, -441.02549]); -marker_left.bindPopup("Matthew Ballard
GitHub: mattrobball"); +var marker_left = L.marker([52.19835, -359.87947]); +marker_left.bindPopup("Eric Wieser
GitHub: eric-wieser"); markers.addLayer(marker_left); -var marker_right = L.marker([33.99825, 278.97451]); -marker_right.bindPopup("Matthew Ballard
GitHub: mattrobball"); +var marker_right = L.marker([52.19835, 360.12053]); +marker_right.bindPopup("Eric Wieser
GitHub: eric-wieser"); markers.addLayer(marker_right); -var marker = L.marker([38.794013, -89.999591]); -marker.bindPopup("Jireh Loreaux
GitHub: j-loreaux"); +var marker = L.marker([49.4, 8.7]); +marker.bindPopup("Junyan Xu
GitHub: alreadydone"); markers.addLayer(marker); -var marker_left = L.marker([38.794013, -449.999591]); -marker_left.bindPopup("Jireh Loreaux
GitHub: j-loreaux"); +var marker_left = L.marker([49.4, -351.3]); +marker_left.bindPopup("Junyan Xu
GitHub: alreadydone"); markers.addLayer(marker_left); -var marker_right = L.marker([38.794013, 270.000409]); -marker_right.bindPopup("Jireh Loreaux
GitHub: j-loreaux"); +var marker_right = L.marker([49.4, 368.7]); +marker_right.bindPopup("Junyan Xu
GitHub: alreadydone"); markers.addLayer(marker_right); -var marker = L.marker([48.119134, -1.641871]); -marker.bindPopup("Sébastien Gouëzel
GitHub: sgouezel"); +var marker = L.marker([44.8125, 20.4612]); +marker.bindPopup("Dragan Okanovic
GitHub: abstractalgo"); markers.addLayer(marker); -var marker_left = L.marker([48.119134, -361.641871]); -marker_left.bindPopup("Sébastien Gouëzel
GitHub: sgouezel"); +var marker_left = L.marker([44.8125, -339.5388]); +marker_left.bindPopup("Dragan Okanovic
GitHub: abstractalgo"); markers.addLayer(marker_left); -var marker_right = L.marker([48.119134, 358.358129]); -marker_right.bindPopup("Sébastien Gouëzel
GitHub: sgouezel"); +var marker_right = L.marker([44.8125, 380.4612]); +marker_right.bindPopup("Dragan Okanovic
GitHub: abstractalgo"); markers.addLayer(marker_right); -var marker = L.marker([34.069364114046024, -118.44351443013207]); -marker.bindPopup("Aaron Anderson
GitHub: awainverse"); +var marker = L.marker([38.9871, -77.21713]); +marker.bindPopup("Hunter Monroe
GitHub: hmonroe"); markers.addLayer(marker); -var marker_left = L.marker([34.069364114046024, -478.44351443013204]); -marker_left.bindPopup("Aaron Anderson
GitHub: awainverse"); +var marker_left = L.marker([38.9871, -437.21713]); +marker_left.bindPopup("Hunter Monroe
GitHub: hmonroe"); markers.addLayer(marker_left); -var marker_right = L.marker([34.069364114046024, 241.55648556986793]); -marker_right.bindPopup("Aaron Anderson
GitHub: awainverse"); +var marker_right = L.marker([38.9871, 282.78287]); +marker_right.bindPopup("Hunter Monroe
GitHub: hmonroe"); markers.addLayer(marker_right); -var marker = L.marker([48.198854, 16.367016]); -marker.bindPopup("Stefan Hetzl
GitHub: shetzl"); +var marker = L.marker([37.55, -121.99]); +marker.bindPopup("Anirudh Rao
GitHub: rao107"); markers.addLayer(marker); -var marker_left = L.marker([48.198854, -343.632984]); -marker_left.bindPopup("Stefan Hetzl
GitHub: shetzl"); +var marker_left = L.marker([37.55, -481.99]); +marker_left.bindPopup("Anirudh Rao
GitHub: rao107"); +markers.addLayer(marker_left); + +var marker_right = L.marker([37.55, 238.01]); +marker_right.bindPopup("Anirudh Rao
GitHub: rao107"); +markers.addLayer(marker_right); + +var marker = L.marker([36.00315447171814, -78.94226527274706]); +marker.bindPopup("Ricardo Prado Cunha
GitHub: MithicSpirit"); +markers.addLayer(marker); + +var marker_left = L.marker([36.00315447171814, -438.9422652727471]); +marker_left.bindPopup("Ricardo Prado Cunha
GitHub: MithicSpirit"); +markers.addLayer(marker_left); + +var marker_right = L.marker([36.00315447171814, 281.0577347272529]); +marker_right.bindPopup("Ricardo Prado Cunha
GitHub: MithicSpirit"); +markers.addLayer(marker_right); + +var marker = L.marker([39.7392, -104.9903]); +marker.bindPopup("Chance Nahuway
GitHub: chancenahuway"); +markers.addLayer(marker); + +var marker_left = L.marker([39.7392, -464.9903]); +marker_left.bindPopup("Chance Nahuway
GitHub: chancenahuway"); +markers.addLayer(marker_left); + +var marker_right = L.marker([39.7392, 255.0097]); +marker_right.bindPopup("Chance Nahuway
GitHub: chancenahuway"); +markers.addLayer(marker_right); + +var marker = L.marker([-22.932126, -43.243052]); +marker.bindPopup("Thiago Andrade
GitHub: 01tpaabr"); +markers.addLayer(marker); + +var marker_left = L.marker([-22.932126, -403.243052]); +marker_left.bindPopup("Thiago Andrade
GitHub: 01tpaabr"); +markers.addLayer(marker_left); + +var marker_right = L.marker([-22.932126, 316.756948]); +marker_right.bindPopup("Thiago Andrade
GitHub: 01tpaabr"); +markers.addLayer(marker_right); + +var marker = L.marker([45.113118, 5.83592]); +marker.bindPopup("Vincent Beffara
GitHub: vbeffara"); +markers.addLayer(marker); + +var marker_left = L.marker([45.113118, -354.16408]); +marker_left.bindPopup("Vincent Beffara
GitHub: vbeffara"); +markers.addLayer(marker_left); + +var marker_right = L.marker([45.113118, 365.83592]); +marker_right.bindPopup("Vincent Beffara
GitHub: vbeffara"); +markers.addLayer(marker_right); + +var marker = L.marker([60.0, 24.0]); +marker.bindPopup("Henrik Lievonen
GitHub: Henkkuli"); +markers.addLayer(marker); + +var marker_left = L.marker([60.0, -336.0]); +marker_left.bindPopup("Henrik Lievonen
GitHub: Henkkuli"); +markers.addLayer(marker_left); + +var marker_right = L.marker([60.0, 384.0]); +marker_right.bindPopup("Henrik Lievonen
GitHub: Henkkuli"); +markers.addLayer(marker_right); + +var marker = L.marker([39.952583, -75.165222]); +marker.bindPopup("Tanner Duve
GitHub: tannerduve"); +markers.addLayer(marker); + +var marker_left = L.marker([39.952583, -435.16522199999997]); +marker_left.bindPopup("Tanner Duve
GitHub: tannerduve"); +markers.addLayer(marker_left); + +var marker_right = L.marker([39.952583, 284.83477800000003]); +marker_right.bindPopup("Tanner Duve
GitHub: tannerduve"); +markers.addLayer(marker_right); + +var marker = L.marker([47.610609, -122.182161]); +marker.bindPopup("Jair Taylor"); +markers.addLayer(marker); + +var marker_left = L.marker([47.610609, -482.182161]); +marker_left.bindPopup("Jair Taylor"); +markers.addLayer(marker_left); + +var marker_right = L.marker([47.610609, 237.817839]); +marker_right.bindPopup("Jair Taylor"); +markers.addLayer(marker_right); + +var marker = L.marker([46.3159, 7.9878]); +marker.bindPopup("David Loeffler
GitHub: loefflerd"); +markers.addLayer(marker); + +var marker_left = L.marker([46.3159, -352.0122]); +marker_left.bindPopup("David Loeffler
GitHub: loefflerd"); +markers.addLayer(marker_left); + +var marker_right = L.marker([46.3159, 367.9878]); +marker_right.bindPopup("David Loeffler
GitHub: loefflerd"); +markers.addLayer(marker_right); + +var marker = L.marker([46.0, -123.0]); +marker.bindPopup("Adam Layne
GitHub: fNBU"); +markers.addLayer(marker); + +var marker_left = L.marker([46.0, -483.0]); +marker_left.bindPopup("Adam Layne
GitHub: fNBU"); +markers.addLayer(marker_left); + +var marker_right = L.marker([46.0, 237.0]); +marker_right.bindPopup("Adam Layne
GitHub: fNBU"); +markers.addLayer(marker_right); + +var marker = L.marker([35.503522, -80.83476]); +marker.bindPopup("Lars Ericson"); +markers.addLayer(marker); + +var marker_left = L.marker([35.503522, -440.83476]); +marker_left.bindPopup("Lars Ericson"); +markers.addLayer(marker_left); + +var marker_right = L.marker([35.503522, 279.16524]); +marker_right.bindPopup("Lars Ericson"); +markers.addLayer(marker_right); + +var marker = L.marker([43.6532, -79.3832]); +marker.bindPopup("Avi Craimer
GitHub: AviCraimer"); +markers.addLayer(marker); + +var marker_left = L.marker([43.6532, -439.3832]); +marker_left.bindPopup("Avi Craimer
GitHub: AviCraimer"); +markers.addLayer(marker_left); + +var marker_right = L.marker([43.6532, 280.6168]); +marker_right.bindPopup("Avi Craimer
GitHub: AviCraimer"); +markers.addLayer(marker_right); + +var marker = L.marker([-16.434067, -51.112691]); +marker.bindPopup("Fabrício S. Paranhos"); +markers.addLayer(marker); + +var marker_left = L.marker([-16.434067, -411.112691]); +marker_left.bindPopup("Fabrício S. Paranhos"); +markers.addLayer(marker_left); + +var marker_right = L.marker([-16.434067, 308.887309]); +marker_right.bindPopup("Fabrício S. Paranhos"); +markers.addLayer(marker_right); + +var marker = L.marker([56.342, -2.796]); +marker.bindPopup("Hyeokjun Kwon
GitHub: Jun2M"); +markers.addLayer(marker); + +var marker_left = L.marker([56.342, -362.796]); +marker_left.bindPopup("Hyeokjun Kwon
GitHub: Jun2M"); +markers.addLayer(marker_left); + +var marker_right = L.marker([56.342, 357.204]); +marker_right.bindPopup("Hyeokjun Kwon
GitHub: Jun2M"); +markers.addLayer(marker_right); + +var marker = L.marker([12.9716, 77.5946]); +marker.bindPopup("Mrigank Pawagi
GitHub: mrigankpawagi"); +markers.addLayer(marker); + +var marker_left = L.marker([12.9716, -282.4054]); +marker_left.bindPopup("Mrigank Pawagi
GitHub: mrigankpawagi"); +markers.addLayer(marker_left); + +var marker_right = L.marker([12.9716, 437.5946]); +marker_right.bindPopup("Mrigank Pawagi
GitHub: mrigankpawagi"); +markers.addLayer(marker_right); + +var marker = L.marker([44.83, -0.57]); +marker.bindPopup("Philippe Duchon"); +markers.addLayer(marker); + +var marker_left = L.marker([44.83, -360.57]); +marker_left.bindPopup("Philippe Duchon"); +markers.addLayer(marker_left); + +var marker_right = L.marker([44.83, 359.43]); +marker_right.bindPopup("Philippe Duchon"); +markers.addLayer(marker_right); + +var marker = L.marker([-22.9, -43.17]); +marker.bindPopup("Henrique Coelho"); +markers.addLayer(marker); + +var marker_left = L.marker([-22.9, -403.17]); +marker_left.bindPopup("Henrique Coelho"); +markers.addLayer(marker_left); + +var marker_right = L.marker([-22.9, 316.83]); +marker_right.bindPopup("Henrique Coelho"); +markers.addLayer(marker_right); + +var marker = L.marker([-35.2813, 149.1183]); +marker.bindPopup("Dom Verity
GitHub: dom-verity@github.com"); +markers.addLayer(marker); + +var marker_left = L.marker([-35.2813, -210.8817]); +marker_left.bindPopup("Dom Verity
GitHub: dom-verity@github.com"); +markers.addLayer(marker_left); + +var marker_right = L.marker([-35.2813, 509.1183]); +marker_right.bindPopup("Dom Verity
GitHub: dom-verity@github.com"); +markers.addLayer(marker_right); + +var marker = L.marker([52.22977, 21.01178]); +marker.bindPopup("Wojciech Nawrocki"); +markers.addLayer(marker); + +var marker_left = L.marker([52.22977, -338.98822]); +marker_left.bindPopup("Wojciech Nawrocki"); +markers.addLayer(marker_left); + +var marker_right = L.marker([52.22977, 381.01178]); +marker_right.bindPopup("Wojciech Nawrocki"); +markers.addLayer(marker_right); + +var marker = L.marker([37.571, 126.977]); +marker.bindPopup("Bulhwi Cha
GitHub: chabulhwi"); +markers.addLayer(marker); + +var marker_left = L.marker([37.571, -233.023]); +marker_left.bindPopup("Bulhwi Cha
GitHub: chabulhwi"); markers.addLayer(marker_left); -var marker_right = L.marker([48.198854, 376.367016]); -marker_right.bindPopup("Stefan Hetzl
GitHub: shetzl"); +var marker_right = L.marker([37.571, 486.977]); +marker_right.bindPopup("Bulhwi Cha
GitHub: chabulhwi"); markers.addLayer(marker_right); -var marker = L.marker([52.334811, 4.864481]); -marker.bindPopup("Sander Dahmen"); +var marker = L.marker([31.2, 121.5]); +marker.bindPopup("Qi Liu
GitHub: Purewhite2019"); markers.addLayer(marker); -var marker_left = L.marker([52.334811, -355.135519]); -marker_left.bindPopup("Sander Dahmen"); +var marker_left = L.marker([31.2, -238.5]); +marker_left.bindPopup("Qi Liu
GitHub: Purewhite2019"); markers.addLayer(marker_left); -var marker_right = L.marker([52.334811, 364.864481]); -marker_right.bindPopup("Sander Dahmen"); +var marker_right = L.marker([31.2, 481.5]); +marker_right.bindPopup("Qi Liu
GitHub: Purewhite2019"); markers.addLayer(marker_right); -var marker = L.marker([32.0717, 34.8469]); -marker.bindPopup("Daniel Weber
GitHub: Command-Master"); +var marker = L.marker([55.944779, -3.187372]); +marker.bindPopup("Ramon Fernández Mir"); markers.addLayer(marker); -var marker_left = L.marker([32.0717, -325.1531]); -marker_left.bindPopup("Daniel Weber
GitHub: Command-Master"); +var marker_left = L.marker([55.944779, -363.187372]); +marker_left.bindPopup("Ramon Fernández Mir"); markers.addLayer(marker_left); -var marker_right = L.marker([32.0717, 394.8469]); -marker_right.bindPopup("Daniel Weber
GitHub: Command-Master"); +var marker_right = L.marker([55.944779, 356.812628]); +marker_right.bindPopup("Ramon Fernández Mir"); markers.addLayer(marker_right); -var marker = L.marker([49.4, 8.7]); -marker.bindPopup("Junyan Xu
GitHub: alreadydone"); +var marker = L.marker([49.4172736001205, 8.67570384259312]); +marker.bindPopup("Florent Schaffhauser
GitHub: matematiflo"); markers.addLayer(marker); -var marker_left = L.marker([49.4, -351.3]); -marker_left.bindPopup("Junyan Xu
GitHub: alreadydone"); +var marker_left = L.marker([49.4172736001205, -351.3242961574069]); +marker_left.bindPopup("Florent Schaffhauser
GitHub: matematiflo"); markers.addLayer(marker_left); -var marker_right = L.marker([49.4, 368.7]); -marker_right.bindPopup("Junyan Xu
GitHub: alreadydone"); +var marker_right = L.marker([49.4172736001205, 368.6757038425931]); +marker_right.bindPopup("Florent Schaffhauser
GitHub: matematiflo"); markers.addLayer(marker_right); -var marker = L.marker([41.715137, 44.827095]); -marker.bindPopup("Evgenia Karunus
GitHub: lakesare"); +var marker = L.marker([20.173226, 85.684102]); +marker.bindPopup("Abhijit Chakraborty
GitHub: Abhijit-niser"); markers.addLayer(marker); -var marker_left = L.marker([41.715137, -315.172905]); -marker_left.bindPopup("Evgenia Karunus
GitHub: lakesare"); +var marker_left = L.marker([20.173226, -274.315898]); +marker_left.bindPopup("Abhijit Chakraborty
GitHub: Abhijit-niser"); markers.addLayer(marker_left); -var marker_right = L.marker([41.715137, 404.827095]); -marker_right.bindPopup("Evgenia Karunus
GitHub: lakesare"); +var marker_right = L.marker([20.173226, 445.684102]); +marker_right.bindPopup("Abhijit Chakraborty
GitHub: Abhijit-niser"); markers.addLayer(marker_right); -var marker = L.marker([43.6532, 79.3832]); -marker.bindPopup("Matthew Bolan
GitHub: mjtb49"); +var marker = L.marker([1.295065068415129, 103.77486870277362]); +marker.bindPopup("Ilya Sergey
GitHub: ilyasergey"); markers.addLayer(marker); -var marker_left = L.marker([43.6532, -280.6168]); -marker_left.bindPopup("Matthew Bolan
GitHub: mjtb49"); +var marker_left = L.marker([1.295065068415129, -256.22513129722637]); +marker_left.bindPopup("Ilya Sergey
GitHub: ilyasergey"); markers.addLayer(marker_left); -var marker_right = L.marker([43.6532, 439.3832]); -marker_right.bindPopup("Matthew Bolan
GitHub: mjtb49"); +var marker_right = L.marker([1.295065068415129, 463.77486870277363]); +marker_right.bindPopup("Ilya Sergey
GitHub: ilyasergey"); markers.addLayer(marker_right); -var marker = L.marker([35.713447207515834, 139.76230247682759]); -marker.bindPopup("Kazuki Takashima
GitHub: kzk-program"); +var marker = L.marker([39.22264454871392, 9.114527859227785]); +marker.bindPopup("Federico Dal Pio Luogo
GitHub: dalps"); markers.addLayer(marker); -var marker_left = L.marker([35.713447207515834, -220.23769752317241]); -marker_left.bindPopup("Kazuki Takashima
GitHub: kzk-program"); +var marker_left = L.marker([39.22264454871392, -350.8854721407722]); +marker_left.bindPopup("Federico Dal Pio Luogo
GitHub: dalps"); markers.addLayer(marker_left); -var marker_right = L.marker([35.713447207515834, 499.7623024768276]); -marker_right.bindPopup("Kazuki Takashima
GitHub: kzk-program"); +var marker_right = L.marker([39.22264454871392, 369.1145278592278]); +marker_right.bindPopup("Federico Dal Pio Luogo
GitHub: dalps"); markers.addLayer(marker_right); -var marker = L.marker([52.19835, 0.12053]); -marker.bindPopup("Eric Wieser
GitHub: eric-wieser"); +var marker = L.marker([53.568059, 9.974478]); +marker.bindPopup("Roman Stehling"); markers.addLayer(marker); -var marker_left = L.marker([52.19835, -359.87947]); -marker_left.bindPopup("Eric Wieser
GitHub: eric-wieser"); +var marker_left = L.marker([53.568059, -350.025522]); +marker_left.bindPopup("Roman Stehling"); markers.addLayer(marker_left); -var marker_right = L.marker([52.19835, 360.12053]); -marker_right.bindPopup("Eric Wieser
GitHub: eric-wieser"); +var marker_right = L.marker([53.568059, 369.974478]); +marker_right.bindPopup("Roman Stehling"); markers.addLayer(marker_right); -var marker = L.marker([44.8125, 20.4612]); -marker.bindPopup("Dragan Okanovic
GitHub: abstractalgo"); +var marker = L.marker([35.713447207515834, 139.76230247682759]); +marker.bindPopup("Kazuki Takashima
GitHub: kzk-program"); markers.addLayer(marker); -var marker_left = L.marker([44.8125, -339.5388]); -marker_left.bindPopup("Dragan Okanovic
GitHub: abstractalgo"); +var marker_left = L.marker([35.713447207515834, -220.23769752317241]); +marker_left.bindPopup("Kazuki Takashima
GitHub: kzk-program"); markers.addLayer(marker_left); -var marker_right = L.marker([44.8125, 380.4612]); -marker_right.bindPopup("Dragan Okanovic
GitHub: abstractalgo"); +var marker_right = L.marker([35.713447207515834, 499.7623024768276]); +marker_right.bindPopup("Kazuki Takashima
GitHub: kzk-program"); markers.addLayer(marker_right); var marker = L.marker([40.236449, -83.367143]); @@ -982,18 +1138,6 @@
Contributing
marker_right.bindPopup("Marcin Wojnarowski
GitHub: shilangyu"); markers.addLayer(marker_right); -var marker = L.marker([-22.932126, -43.243052]); -marker.bindPopup("Thiago Andrade
GitHub: 01tpaabr"); -markers.addLayer(marker); - -var marker_left = L.marker([-22.932126, -403.243052]); -marker_left.bindPopup("Thiago Andrade
GitHub: 01tpaabr"); -markers.addLayer(marker_left); - -var marker_right = L.marker([-22.932126, 316.756948]); -marker_right.bindPopup("Thiago Andrade
GitHub: 01tpaabr"); -markers.addLayer(marker_right); - var marker = L.marker([26.3088521, 50.1428595]); marker.bindPopup("Khaled Alshehri"); markers.addLayer(marker); @@ -1018,18 +1162,6 @@
Contributing
marker_right.bindPopup("Newell Jensen
GitHub: newell"); markers.addLayer(marker_right); -var marker = L.marker([45.113118, 5.83592]); -marker.bindPopup("Vincent Beffara
GitHub: vbeffara"); -markers.addLayer(marker); - -var marker_left = L.marker([45.113118, -354.16408]); -marker_left.bindPopup("Vincent Beffara
GitHub: vbeffara"); -markers.addLayer(marker_left); - -var marker_right = L.marker([45.113118, 365.83592]); -marker_right.bindPopup("Vincent Beffara
GitHub: vbeffara"); -markers.addLayer(marker_right); - var marker = L.marker([48.262587, 11.667908]); marker.bindPopup("Andreas Vollert
GitHub: hydrogenoxide"); markers.addLayer(marker); @@ -1042,18 +1174,6 @@
Contributing
marker_right.bindPopup("Andreas Vollert
GitHub: hydrogenoxide"); markers.addLayer(marker_right); -var marker = L.marker([60.0, 24.0]); -marker.bindPopup("Henrik Lievonen
GitHub: Henkkuli"); -markers.addLayer(marker); - -var marker_left = L.marker([60.0, -336.0]); -marker_left.bindPopup("Henrik Lievonen
GitHub: Henkkuli"); -markers.addLayer(marker_left); - -var marker_right = L.marker([60.0, 384.0]); -marker_right.bindPopup("Henrik Lievonen
GitHub: Henkkuli"); -markers.addLayer(marker_right); - var marker = L.marker([32.593357, -85.495163]); marker.bindPopup("Yimin Zhong
GitHub: lowrank"); markers.addLayer(marker); @@ -1066,66 +1186,6 @@
Contributing
marker_right.bindPopup("Yimin Zhong
GitHub: lowrank"); markers.addLayer(marker_right); -var marker = L.marker([39.952583, -75.165222]); -marker.bindPopup("Tanner Duve
GitHub: tannerduve"); -markers.addLayer(marker); - -var marker_left = L.marker([39.952583, -435.16522199999997]); -marker_left.bindPopup("Tanner Duve
GitHub: tannerduve"); -markers.addLayer(marker_left); - -var marker_right = L.marker([39.952583, 284.83477800000003]); -marker_right.bindPopup("Tanner Duve
GitHub: tannerduve"); -markers.addLayer(marker_right); - -var marker = L.marker([46.3159, 7.9878]); -marker.bindPopup("David Loeffler
GitHub: loefflerd"); -markers.addLayer(marker); - -var marker_left = L.marker([46.3159, -352.0122]); -marker_left.bindPopup("David Loeffler
GitHub: loefflerd"); -markers.addLayer(marker_left); - -var marker_right = L.marker([46.3159, 367.9878]); -marker_right.bindPopup("David Loeffler
GitHub: loefflerd"); -markers.addLayer(marker_right); - -var marker = L.marker([46.0, -123.0]); -marker.bindPopup("Adam Layne
GitHub: fNBU"); -markers.addLayer(marker); - -var marker_left = L.marker([46.0, -483.0]); -marker_left.bindPopup("Adam Layne
GitHub: fNBU"); -markers.addLayer(marker_left); - -var marker_right = L.marker([46.0, 237.0]); -marker_right.bindPopup("Adam Layne
GitHub: fNBU"); -markers.addLayer(marker_right); - -var marker = L.marker([56.342, -2.796]); -marker.bindPopup("Hyeokjun Kwon
GitHub: Jun2M"); -markers.addLayer(marker); - -var marker_left = L.marker([56.342, -362.796]); -marker_left.bindPopup("Hyeokjun Kwon
GitHub: Jun2M"); -markers.addLayer(marker_left); - -var marker_right = L.marker([56.342, 357.204]); -marker_right.bindPopup("Hyeokjun Kwon
GitHub: Jun2M"); -markers.addLayer(marker_right); - -var marker = L.marker([44.83, -0.57]); -marker.bindPopup("Philippe Duchon"); -markers.addLayer(marker); - -var marker_left = L.marker([44.83, -360.57]); -marker_left.bindPopup("Philippe Duchon"); -markers.addLayer(marker_left); - -var marker_right = L.marker([44.83, 359.43]); -marker_right.bindPopup("Philippe Duchon"); -markers.addLayer(marker_right); - var marker = L.marker([51.3397, 12.3731]); marker.bindPopup("Abhiram M K
GitHub: abhirammk"); markers.addLayer(marker); @@ -1174,66 +1234,6 @@
Contributing
marker_right.bindPopup("Torger Olson"); markers.addLayer(marker_right); -var marker = L.marker([52.22977, 21.01178]); -marker.bindPopup("Wojciech Nawrocki"); -markers.addLayer(marker); - -var marker_left = L.marker([52.22977, -338.98822]); -marker_left.bindPopup("Wojciech Nawrocki"); -markers.addLayer(marker_left); - -var marker_right = L.marker([52.22977, 381.01178]); -marker_right.bindPopup("Wojciech Nawrocki"); -markers.addLayer(marker_right); - -var marker = L.marker([37.571, 126.977]); -marker.bindPopup("Bulhwi Cha
GitHub: chabulhwi"); -markers.addLayer(marker); - -var marker_left = L.marker([37.571, -233.023]); -marker_left.bindPopup("Bulhwi Cha
GitHub: chabulhwi"); -markers.addLayer(marker_left); - -var marker_right = L.marker([37.571, 486.977]); -marker_right.bindPopup("Bulhwi Cha
GitHub: chabulhwi"); -markers.addLayer(marker_right); - -var marker = L.marker([31.2, 121.5]); -marker.bindPopup("Qi Liu
GitHub: Purewhite2019"); -markers.addLayer(marker); - -var marker_left = L.marker([31.2, -238.5]); -marker_left.bindPopup("Qi Liu
GitHub: Purewhite2019"); -markers.addLayer(marker_left); - -var marker_right = L.marker([31.2, 481.5]); -marker_right.bindPopup("Qi Liu
GitHub: Purewhite2019"); -markers.addLayer(marker_right); - -var marker = L.marker([55.944779, -3.187372]); -marker.bindPopup("Ramon Fernández Mir"); -markers.addLayer(marker); - -var marker_left = L.marker([55.944779, -363.187372]); -marker_left.bindPopup("Ramon Fernández Mir"); -markers.addLayer(marker_left); - -var marker_right = L.marker([55.944779, 356.812628]); -marker_right.bindPopup("Ramon Fernández Mir"); -markers.addLayer(marker_right); - -var marker = L.marker([49.4172736001205, 8.67570384259312]); -marker.bindPopup("Florent Schaffhauser
GitHub: matematiflo"); -markers.addLayer(marker); - -var marker_left = L.marker([49.4172736001205, -351.3242961574069]); -marker_left.bindPopup("Florent Schaffhauser
GitHub: matematiflo"); -markers.addLayer(marker_left); - -var marker_right = L.marker([49.4172736001205, 368.6757038425931]); -marker_right.bindPopup("Florent Schaffhauser
GitHub: matematiflo"); -markers.addLayer(marker_right); - var marker = L.marker([44.40362300559697, 8.972344520676371]); marker.bindPopup("Francesco Veneziano
GitHub: fvenez"); markers.addLayer(marker);