Commit 2025-02-10 20:43 5dc48857

View on Github →

feat(CategoryTheory): group objects in the category of types (#21576)

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/CategoryTheory/Monoidal/Internal/Types.lean to Mathlib/CategoryTheory/Monoidal/Internal/Types/Basic.lean

Created Mathlib/CategoryTheory/Monoidal/Internal/Types/Grp_.lean

Modified Mathlib/CategoryTheory/Monoidal/Types/Basic.lean

added theorem CategoryTheory.ChosenFiniteProducts.lift_apply