-
Notifications
You must be signed in to change notification settings - Fork 298
/
overview.yaml
386 lines (359 loc) · 15.5 KB
/
overview.yaml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
General algebra:
Category theory:
category: 'category_theory.category'
small category: 'category_theory.small_category'
functor: 'category_theory.functor'
natural transformation: 'category_theory.nat_trans'
Yoneda embedding: 'category_theory.yoneda'
adjunction: 'category_theory.adjunction'
monad: 'category_theory.monad'
comma category: 'category_theory.comma'
limits: 'category_theory.limits.is_limit'
presheafed space: 'algebraic_geometry.PresheafedSpace'
sheafed space: 'algebraic_geometry.SheafedSpace'
monoidal category: 'category_theory.monoidal_category'
cartesian closed: 'category_theory.cartesian_closed'
abelian category: 'category_theory.abelian'
Numbers:
natural number: 'nat'
integer: 'int'
rational number: 'rat'
continued fraction: 'continued_fraction'
real number: 'real'
extended real number: 'ereal'
complex number: 'complex'
"$p$-adic number": 'padic'
"$p$-adic integer": 'padic_int'
hyper-real number: 'hyperreal'
Group theory:
group: 'group'
group morphism: 'monoid_hom'
subgroup: 'subgroup'
subgroup generated by a subset: 'subgroup.closure'
quotient group: 'quotient_group.quotient.group'
first isomorphism theorem: 'quotient_add_group.quotient_ker_equiv_range'
abelianization: 'abelianization'
free group: 'free_group'
group action: 'mul_action'
cyclic group: 'is_cyclic'
permutation group of a type: 'equiv.perm'
Rings:
ring: 'ring'
ring morphism: 'ring_hom'
the category of rings: 'Ring'
subring: 'is_subring'
local ring: 'local_ring'
noetherian ring: 'is_noetherian_ring'
ordered ring: 'ordered_ring'
Ideals and quotients:
ideal of a commutative ring: 'ideal'
quotient ring: 'ideal.quotient'
prime ideal: 'ideal.is_prime'
maximal ideal: 'ideal.is_maximal'
Chinese remainder theorem: 'ideal.quotient_inf_ring_equiv_pi_quotient'
localization: 'localization'
fractional ideal: 'ring.fractional_ideal'
first isomorphism theorem for commutative rings: 'ring_hom.quotient_ker_equiv_of_surjective'
Divisibility in integral domains:
irreducible element: 'irreducible'
coprime element: 'is_coprime'
unique factorisation domain: 'unique_factorization_monoid'
greatest common divisor: 'gcd_monoid.gcd'
least common multiple: 'gcd_monoid.lcm'
principal ideal domain: 'submodule.is_principal'
Euclidean domain: 'euclidean_domain'
Euclid's' algorithm: 'nat.xgcd'
Euler's totient function ($\varphi$): 'nat.totient'
Lucas-Lehmer primality test: 'lucas_lehmer_sufficiency'
Polynomials and power series:
polynomial in one indeterminate: 'polynomial'
roots of a polynomial: 'polynomial.roots'
multiplicity: 'polynomial.root_multiplicity'
separable polynomial: 'polynomial.separable'
$K[X]$ is Euclidean: 'polynomial.euclidean_domain'
Hilbert basis theorem: 'polynomial.is_noetherian_ring'
$A[X]$ has gcd and lcm if $A$ does: 'polynomial.gcd_monoid'
$A[X]$ is a UFD when $A$ is a UFD: 'polynomial.unique_factorization_monoid'
irreducible polynomial: 'irreducible'
Eisenstein's criterion: 'polynomial.irreducible_of_eisenstein_criterion'
polynomial in several indeterminates: 'mv_polynomial'
power series: 'power_series'
Algebras over a ring:
associative algebra over a commutative ring: 'algebra'
the category of algebras over a ring: 'Algebra'
free algebra of a commutative ring: 'free_algebra'
tensor product of algebras: 'algebra.tensor_product.tensor_product.algebra'
tensor algebra of a commutative ring: 'tensor_algebra'
Lie algebra: 'lie_algebra'
exterior algebra: 'exterior_algebra'
Clifford algebra: 'clifford_algebra'
Field theory:
field: 'field'
characteristic of a ring: 'ring_char'
characteristic zero: 'char_zero'
characteristic p: 'char_p'
Frobenius morphism: 'frobenius'
algebraically closed field: 'is_alg_closed'
existence of algebraic closure of a field: 'algebraic_closure'
$\C$ is algebraically closed: 'complex.exists_root'
field of fractions of an integral domain: 'fraction_map'
algebraic extension: 'algebra.is_algebraic'
rupture field: 'adjoin_root'
splitting field: 'polynomial.splitting_field'
perfect closure: 'perfect_closure'
Galois correspondence: 'is_galois.intermediate_field_equiv_subgroup'
Abel-Ruffini theorem (one direction): 'solvable_by_rad.is_solvable'
Homological algebra:
chain complex: 'chain_complex'
functorial homology: 'homological_complex.homology'
Number theory:
sum of two squares: 'nat.prime.sum_two_squares'
sum of four squares: 'nat.sum_four_squares'
quadratic reciprocity: 'zmod.quadratic_reciprocity'
"solutions to Pell's equation": 'pell.pell'
"Matiyasevič's theorem": 'pell.matiyasevic'
arithmetic functions: 'nat.arithmetic_function'
Bernoulli numbers: 'bernoulli'
Chevalley-Warning theorem: 'char_dvd_card_solutions'
"Hensel's lemma (for $\\mathbb{Z}_p$)": 'hensels_lemma'
ring of Witt vectors: 'witt_vector'
perfection of a ring: 'ring.perfection'
Linear algebra:
Fundamentals:
module: 'module'
linear map: 'linear_map'
the category of modules over a ring: 'Module'
vector space: 'module'
quotient space: 'submodule.quotient'
tensor product: 'tensor_product'
noetherian module: 'is_noetherian'
basis: 'is_basis'
multilinear map: 'multilinear_map'
alternating map: 'alternating_map'
general linear group: 'linear_map.general_linear_group'
Duality:
dual vector space: 'module.dual'
dual basis: 'is_basis.dual_basis'
Finite-dimensional vector spaces:
finite-dimensionality : 'finite_dimensional'
isomorphism with $K^n$: 'module_equiv_finsupp'
isomorphism with bidual: 'module.eval_equiv'
Matrices:
ring-valued matrix: 'matrix'
matrix representation of a linear map: 'linear_map.to_matrix'
determinant: 'matrix.det'
invertibility: 'matrix.nonsing_inv'
Endomorphism polynomials:
minimal polynomial: 'minpoly'
characteristic polynomial: 'char_poly'
Cayley-Hamilton theorem: 'aeval_self_char_poly'
Structure theory of endomorphisms:
eigenvalue: 'module.End.has_eigenvalue'
eigenvector: 'module.End.has_eigenvector'
existence of an eigenvalue: 'module.End.exists_eigenvalue'
Bilinear and quadratic forms:
bilinear form: 'bilin_form'
alternating bilinear form: 'alt_bilin_form.is_alt'
symmetric bilinear form: 'sym_bilin_form.is_sym'
matrix representation: 'bilin_form.to_matrix'
quadratic form: 'quadratic_form'
polar form of a quadratic: 'quadratic_form.polar'
Euclidean vector space: 'inner_product_space'
Cauchy-Schwarz inequality: 'inner_mul_inner_self_le'
self-adjoint endomorphism: 'bilin_form.is_self_adjoint'
Topology:
General topology:
filter: 'filter'
limit of a map with respect to filters: 'filter.tendsto'
topological space: 'topological_space'
continuous function: 'continuous'
the category of topological spaces: 'Top'
induced topology: 'topological_space.induced'
open map: 'is_open_map'
closed map: 'is_closed_map'
closure: 'closure'
cluster point: 'cluster_pt'
Hausdorff space: 't2_space'
sequential space: 'sequential_space'
extension by continuity: 'dense_inducing.extend'
compactness in terms of filters: 'is_compact'
compactness in terms of open covers (Borel-Lebesgue): 'compact_iff_finite_subcover'
connectedness: 'connected_space'
compact open topology: 'continuous_map.compact_open'
Stone-Cech compactification: 'stone_cech'
topological fiber bundle: 'is_topological_fiber_bundle'
Uniform notions:
uniform space: 'uniform_space'
uniformly continuous function: 'metric.uniform_continuous_iff'
uniform convergence: 'tendsto_uniformly'
Cauchy filter: 'cauchy'
Cauchy sequence: 'cauchy_seq'
completeness: 'complete_space'
completion: 'completion'
Heine-Cantor theorem: 'compact_space.uniform_continuous_of_continuous'
Topological algebra:
order topology: 'order_topology'
intermediate value theorem: 'intermediate_value_Icc'
extreme value theorem: 'is_compact.exists_forall_le'
limit infimum and supremum: 'order/liminf_limsup.html'
topological group: 'topological_group'
completion of an abelian topological group: 'uniform_space.completion.add_comm_group '
infinite sum: 'has_sum'
topological ring: 'topological_ring'
completion of a topological ring: 'uniform_space.completion.ring'
topological module: 'has_continuous_smul'
Haar measure on a locally compact Hausdorff group: 'measure_theory.measure.haar_measure'
Metric spaces:
metric space: 'metric_space'
ball: 'metric.ball'
sequential compactness is equivalent to compactness (Bolzano-Weierstrass): 'metric.compact_iff_seq_compact'
Heine-Borel theorem (proper metric space version): 'metric.compact_iff_closed_bounded'
Lipschitz function: 'lipschitz_with'
contraction mapping theorem: 'contracting_with.exists_fixed_point'
Baire theorem: 'dense_Inter_of_open'
Arzela-Ascoli theorem: 'bounded_continuous_function.arzela_ascoli'
Hausdorff distance: ' emetric.Hausdorff_edist'
Gromov-Hausdorff space: 'Gromov_Hausdorff.GH_space'
Analysis:
Normed vector spaces:
normed vector space over a normed field: 'normed_space'
topology on a normed vector space: 'semi_normed_space.has_continuous_smul'
equivalence of norms in finite dimension: 'linear_equiv.to_continuous_linear_equiv'
finite dimensional normed spaces over complete normed fields are complete: 'submodule.complete_of_finite_dimensional'
Heine-Borel theorem (finite dimensional normed spaces are proper): 'finite_dimensional.proper'
continuous linear map: 'continuous_linear_map'
norm of a continuous linear map: 'linear_map.mk_continuous'
Banach open mapping theorem: 'open_mapping'
absolutely convergent series in Banach spaces: 'summable_of_summable_norm'
Hahn-Banach theorem: 'exists_extension_norm_eq'
dual of a normed space: 'normed_space.dual'
Fréchet-Riesz representation of the dual of a Hilbert space: 'inner_product_space.to_dual'
isometric inclusion in double dual: 'normed_space.inclusion_in_double_dual_isometry'
completeness of spaces of bounded continuous functions: 'bounded_continuous_function.complete_space'
Differentiability:
differentiable function between normed vector spaces: 'has_fderiv_at'
derivative of a composition of functions: 'has_fderiv_at.comp'
derivative of the inverse of a function: 'has_fderiv_at.of_local_left_inverse'
Rolle's theorem: 'exists_deriv_eq_zero'
mean value theorem: 'exists_ratio_deriv_eq_ratio_slope'
$C^k$ function: 'times_cont_diff'
Leibniz formula: 'fderiv_mul'
local extrema: 'is_local_min.fderiv_eq_zero'
inverse function theorem: 'has_strict_fderiv_at.to_local_inverse'
implicit function theorem: 'implicit_function_data.implicit_function'
analytic function: 'analytic_at'
Convexity:
convex function: 'convex_on'
characterization of convexity: 'convex_on_of_deriv2_nonneg'
Jensen's inequality (finite sum version): 'convex_on.map_sum_le'
Jensen's inequality (integral version): 'convex_on.map_integral_le'
convexity inequalities: 'analysis/mean_inequalities.html'
Carathéodory's theorem: 'convex_hull_eq_union'
Special functions:
logarithm: 'real.log'
exponential: 'real.exp'
trigonometric functions: 'real.sin'
inverse trigonometric functions: 'real.arcsin'
hyperbolic trigonometric functions: 'real.sinh'
inverse hyperbolic trigonometric functions: 'real.arsinh'
Measures and integral calculus:
sigma-algebra: 'measurable_space'
measurable function: 'measurable'
the category of measurable spaces: 'Meas'
Borel sigma-algebra: 'borel_space'
positive measure: 'measure_theory.measure'
Lebesgue measure: 'measure_theory.real.measure_space'
Giry monad: 'measure_theory.measure.measurable_space'
integral of positive measurable functions: 'measure_theory.lintegral'
monotone convergence theorem: 'measure_theory.lintegral_infi_ae'
Fatou's lemma: 'measure_theory.lintegral_liminf_le'
vector-valued integrable function (Bochner integral): 'measure_theory.integrable'
$L^p$ space: 'measure_theory.Lp'
Bochner integral: 'measure_theory.integral'
dominated convergence theorem: 'measure_theory.tendsto_integral_of_dominated_convergence'
fundamental theorem of calculus, part 1: 'interval_integral.integral_has_fderiv_at_of_tendsto_ae'
fundamental theorem of calculus, part 2: 'interval_integral.integral_eq_sub_of_has_deriv_right_of_le'
Fubini's theorem: 'measure_theory.integral_prod'
product of finitely many measures: 'measure_theory.measure.pi'
Geometry:
Affine and Euclidean geometry:
affine space: 'add_torsor'
affine function: 'affine_map'
affine subspace: 'affine_subspace'
barycenter: 'finset.affine_combination'
affine span: 'span_points'
Euclidean affine space: 'normed_add_torsor'
angle: ' inner_product_geometry.angle'
Differentiable manifolds:
smooth manifold (with boundary and corners): 'smooth_manifold_with_corners'
smooth map between manifolds: 'mdifferentiable_at'
tangent bundle: 'tangent_bundle'
tangent map: 'tangent_map'
Lie group: 'lie_group'
sphere: 'metric.sphere.smooth_manifold_with_corners'
Algebraic geometry:
prime spectrum: 'prime_spectrum'
Zariski topology: 'prime_spectrum.zariski_topology'
locally ringed space: 'algebraic_geometry.LocallyRingedSpace'
scheme: 'algebraic_geometry.Scheme'
Nullstellensatz : 'mv_polynomial.vanishing_ideal_zero_locus_eq_radical'
Combinatorics:
Graph theory:
simple graph: 'simple_graph'
degree-sum formula: 'simple_graph.sum_degrees_eq_twice_card_edges'
matching: 'simple_graph.matching'
adjacency matrix: 'simple_graph.adj_matrix'
Pigeonhole principles:
finite: 'fintype.exists_ne_map_eq_of_card_lt'
infinite: 'fintype.exists_infinite_fiber'
strong pigeonhole principle: 'fintype.exists_lt_card_fiber_of_mul_lt_card'
Transversals:
Hall's marriage theorem: 'finset.all_card_le_bUnion_card_iff_exists_injective'
Dynamics:
Circle dynamics:
translation number: 'circle_deg1_lift.translation_number'
translation numbers define a group action up to semiconjugacy:
'circle_deg1_lift.semiconj_of_group_action_of_forall_translation_number_eq'
translation number defines a homeomorphism up to semiconjugacy:
'circle_deg1_lift.semiconj_of_bijective_of_translation_number_eq'
General theory:
omega-limit sets: 'omega_limit'
fixed points: 'function.fixed_points'
periodic points: 'function.periodic_pts'
Data structures:
List-like structures:
list: 'list'
array: 'array'
buffer: 'buffer'
difference list: 'dlist'
lazy list: 'lazy_list'
stream: 'stream'
sequence: 'seq'
weak sequence: 'wseq'
Sets:
set: 'set'
finite set: 'finset'
multiset: 'multiset'
ordered set: 'ordset'
Maps:
key-value map: 'alist'
red-black map: 'rbmap'
hash map: 'hash_map'
finitely supported function: 'finsupp'
finite map: 'finmap'
Trees:
tree: 'tree'
red-black tree: 'rbtree'
size-balanced binary search tree: 'ordnode'
W type: 'W_type'
Logic and computation:
Computability:
computable function: 'computable'
Turing machine: 'turing.TM0.machine'
halting problem: 'computable_pred.halting_problem'
Rice theorem: 'computable_pred.rice'
combinatorial game: 'game'
Set theory:
ordinal: 'ordinal'
cardinal: 'cardinal'
model of ZFC: 'Set'