Commit 2025-02-05 17:15 6aadd7f3

View on Github →

refactor(CategoryTheory): ConcreteCategory instance for FintypeCat (#21466) Upgrade the HasForget instance on FintypeCat to a ConcreteCategory.

Estimated changes

Modified Mathlib/CategoryTheory/FintypeCat.lean

deleted def FintypeCat.of

added structure FintypeCat

deleted def FintypeCat

Modified Mathlib/CategoryTheory/Preadditive/Mat.lean

Modified Mathlib/Order/Category/FinPartOrd.lean