Commit 2026-03-12 17:39 1174c641

View on Github →

refactor(CategoryTheory/FintypeCat): redefine FintypeCat as a full subcategory of Type (#36498)

Estimated changes

Modified Mathlib/CategoryTheory/FintypeCat.lean

modified theorem FintypeCat.Skeleton.incl_mk_nat_card

modified theorem FintypeCat.id_hom

deleted def FintypeCat.incl

deleted structure FintypeCat

Modified Mathlib/CategoryTheory/Galois/Basic.lean

Modified Mathlib/CategoryTheory/Galois/Decomposition.lean

Modified Mathlib/CategoryTheory/Galois/Equivalence.lean

Modified Mathlib/CategoryTheory/Galois/EssSurj.lean

Modified Mathlib/CategoryTheory/Galois/Examples.lean

Modified Mathlib/CategoryTheory/Galois/GaloisObjects.lean

Modified Mathlib/CategoryTheory/Galois/Topology.lean

Modified Mathlib/CategoryTheory/Preadditive/Mat.lean

Modified Mathlib/Condensed/Discrete/Colimit.lean

Modified Mathlib/Order/Category/FinBoolAlg.lean

deleted def fintypeToFinBoolAlgOp

Modified Mathlib/Topology/Category/LightProfinite/Basic.lean

Modified Mathlib/Topology/Category/Profinite/AsLimit.lean

Modified Mathlib/Topology/Category/Profinite/Basic.lean