Mathlib Map

Map · 40

sequences and series

MSC 40 · Sequences, series, summability

1,247 declarations (1,190 theorems, 57 definitions) across 21 files. 0 of the 3 famous theorems listed for this area are in Mathlib (0%). 10 open conjectures here are stated in Lean.

Files are assigned to areas by a language model reading each file's documentation. Report a file that is in the wrong area.

Subareas1

  • 40A Convergence and divergence of infinite limiting processes 1,247

Famous theorems0 of 3

From the 1000+ theorems project, which classifies each theorem by MSC area.

Not yet in Mathlib · 3

From the 100 theorems list2

Open conjectures stated in Lean10

Statements without proofs, collected by the Formal Conjectures project.

Structures defined here4

Typeclasses defined in this area's files, most assumed first.

Files21

Largest first. The code after each file is its assigned subarea.