Mathlib Map

Map · 17

nonassociative algebras

MSC 17 · Nonassociative rings and algebras

4,141 declarations (3,021 theorems, 1,120 definitions) across 97 files. 0 of the 9 famous theorems listed for this area are in Mathlib (0%). 2 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.

Subareas3

  • 17B Lie algebras and Lie superalgebras 3,502
  • 17A General nonassociative rings 619
  • 17C Jordan algebras (algebras, triples and pairs) 20

Famous theorems0 of 9

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

Not yet in Mathlib · 9

Open conjectures stated in Lean2

Statements without proofs, collected by the Formal Conjectures project.

Structures defined here24

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

Files97

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