Build software better, together

Projects

Divided Powers
#25 updated Feb 28, 2025
Linear topologies and formal series evaluation
#24 updated Feb 19, 2025
Classification of semisimple Lie algebras
#17 updated Feb 16, 2025

The goal is to add the classification of finite-dimensional semisimple Lie algebras over algebraically-closed fields of characteristic zero to Mathlib.
Derivatives in Topological Vector Spaces
#21 updated Jan 28, 2025

Making `fderiv` and lemmas about it work in topological vector spaces, so that no choice of norm has to be made.
Exponential map on Lie groups
#16 updated Nov 27, 2024
Ramsey theory
#22 updated Nov 12, 2024

PRs from the exponential Ramsey project
Infinity category theory
#18 updated Sep 4, 2024

A project to coordinate work on the development of infinity category theory
Teaching Features
#3 updated Jul 8, 2024
Class number formula
#20 updated Apr 29, 2024

Let's prove the class number formula.
Homeomorphism between convex sets
#8 updated Feb 22, 2024
Covering spaces and étale spaces
#13 updated Jan 28, 2024
Toward solid abelian groups
#15 updated Dec 5, 2023
Graded rings, modules, and algebras
#1 updated Oct 26, 2023
Mathlib4 freezing targets
#6 updated Oct 26, 2023
Transition to Lean 4 / mathlib4
#5 updated Oct 26, 2023
Normal form of `x ↦ ax + O(x^{1+ε})`, `0<|a|<1`
#10 updated Oct 26, 2023
Two-sided ideals
#11 updated Oct 25, 2023
Ergodicity of the irrational rotation
#7 updated Jul 27, 2023
Define de Rham cohomologies
#9 updated Jul 6, 2023

Provide feedback