Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-05-13 21:42
9eecc5f5
View on Github →
chore(CategoryTheory/Idempotents): fix simp direction in Karoubi (
#24848
)
Estimated changes
Modified
Mathlib/CategoryTheory/Idempotents/FunctorExtension.lean
Modified
Mathlib/CategoryTheory/Idempotents/Karoubi.lean
modified
theorem
CategoryTheory.Idempotents.Karoubi.p_comp