FintypeCat.fintype

{X : FintypeCat} → Fintype X.obj

A Fintype instance on objects on FintypeCat, that should be turned on as needed. Prefer the Finite instance if possible.

Defined in: Mathlib.CategoryTheory.FintypeCat
Cited by: 5 results in Mathlib
Foundations: Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Fintypestatement · cited by 7,736
Finitestatement · cited by 3,029
CategoryTheory.ObjectProperty.FullSubcategory.objstatement and proof · cited by 1,316
Fintype.ofFiniteproof · cited by 255
FintypeCatstatement and proof · cited by 217

Results whose statement or proof uses this declaration.