Mathlib informalized

Statements of Mathlib (commit c31114ff81), each with its Lean source, its translation to Dedukti by Export.lean, and its informalization by Informath, in English, as a formula, and in French, Czech, German and Swedish, which the buttons at each entry show there, and the check boxes above the entries everywhere. The Dedukti translation drops implicit and instance arguments and maps Lean's arithmetic and logic to Informath's base (mapping.tsv); the other Mathlib constants are worded by the symbol table mathlib.dkgf, whose English wordings Informath also renders in the other languages. Constants without a wording appear as $\mathrm{name}$.

One page for each part of Mathlib:

part of Mathlib	statements	fully worded, English	French	Czech	German	Swedish
Mathlib.Order.Defs	354	291	289	289	248	289
Prop	2	1	1	1	1	1
Unbundled	103	73	71	71	69	71
PartialOrder	65	58	58	58	58	58
LinearOrder	78	56	56	56	52	56
Lattice	106	103	103	103	68	103
Mathlib.Algebra	29	29	29	29	28	28
Group.Nat.Units	4	4	4	4	4	4
Prime.Defs	25	25	25	25	24	24
Mathlib.Data.Nat.Prime	128	125	125	125	125	125
Defs	65	63	63	63	63	63
Basic	55	55	55	55	55	55
Factorial	4	4	4	4	4	4
Infinite	2	1	1	1	1	1
Pow	2	2	2	2	2	2
Mathlib.Data.Nat.Factorization	194	143	143	143	132	142
Defs	47	34	34	34	34	34
Basic	78	65	65	65	55	65
Divisors	8	2	2	2	2	2
Induction	8	0	0	0	0	0
LCM	10	10	10	10	10	10
PrimePow	19	13	13	13	13	13
Root	24	19	19	19	18	18
all	705	588	586	586	533	584

All of Mathlib's definitions in English ›25,857 of its 38,690 definitions (functions, types, structures, classes, predicates) have an English wording, made from their docstrings and names; search them by name, wording or docstring, by part of Mathlib and by kind.