Freyd-Mitchell and Gabriel-Popescu
Earlier this year, Jakob von Raumer, Paul Reichert and I finished a long project adding the Freyd-Mitchell and Gabriel-Popescu theorems to mathlib, Lean’s mathematical library. This week, a blog post about the project went live on the Lean community blog. Click here to read it!