Mathlib Map

Map · 13

commutative algebra

MSC 13 · Commutative algebra

24,215 declarations (19,613 theorems, 4,602 definitions) across 809 files. 7 of the 15 famous theorems listed for this area are in Mathlib (47%). 3 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.

Subareas12

  • 13B Commutative ring extensions and related topics 5,526
  • 13A General commutative ring theory 5,260
  • 13C Theory of modules and ideals in commutative rings 4,494
  • 13F Arithmetic rings and other special commutative rings 2,737
  • 13J Topological rings and modules 2,293
  • 13P Computational aspects and applications of commutative rings 1,246
  • 13H Local rings and semilocal rings 893
  • 13G Integral domains 618
  • 13N Differential algebra 527
  • 13E Chain conditions, finiteness conditions in commutative ring theory 379
  • 13D Homological methods in commutative ring theory 223
  • 13M Finite commutative rings 19

Famous theorems7 of 15

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

Not yet in Mathlib · 8

In Mathlib · 7

From the 100 theorems list1

Open conjectures stated in Lean3

Statements without proofs, collected by the Formal Conjectures project.

Undergraduate topics still missing3 of 61

From Mathlib's own undergraduate checklist.

Ring Theory · 3 of 61

  • Algebra › algebra over a commutative ring
  • Field Theory › $\R(X)$-partial fraction decomposition
  • Field Theory › $\C(X)$-partial fraction decomposition

Structures defined here24

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

Files809

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