Mathlib Map

Map · 16

ring theory

MSC 16 · Associative rings and algebras

11,302 declarations (8,157 theorems, 3,145 definitions) across 251 files. 6 of the 11 famous theorems listed for this area are in Mathlib (55%). 8 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.

Subareas11

  • 16S Associative rings and algebras arising under various constructions 3,425
  • 16D Modules, bimodules and ideals in associative algebras 2,697
  • 16W Associative rings and algebras with additional structure 2,031
  • 16B General and miscellaneous 881
  • 16T Hopf algebras, quantum groups and related topics 859
  • 16H Associative algebras and orders 816
  • 16U Conditions on elements 230
  • 16Y Generalizations 142
  • 16K Division rings and semisimple Artin rings 107
  • 16P Chain conditions, growth conditions, and other forms of finiteness for associative rings and algebras 25
  • 16L Local rings and generalizations 11

Famous theorems6 of 11

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

Not yet in Mathlib · 5

In Mathlib · 6

Open conjectures stated in Lean8

Statements without proofs, collected by the Formal Conjectures project.

Structures defined here24

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

Files251

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