Theorems · Definition · combinatorics
Fintype.ofFinite
(α : Type u_4) → [Finite α] → Fintype α
Noncomputably get a Fintype instance from a Finite instance. This is not an
instance because we want Fintype instances to be useful for computations.
- Defined in
- Mathlib.Data.Fintype.EquivFin
- Cited by
- 255 results in Mathlib
- Foundations
- Depth 60 from the axioms, rests on 943 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- Finite
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypestatement · cited by 7,736
- Finitestatement and proof · cited by 3,029
- Nonempty.someproof · cited by 340
- nonempty_fintypeproof · cited by 261
Cited by272
Results whose statement or proof uses this declaration.
- Finite.one_lt_card_iff_nontrivialproof · cited by 11
- Nat.card_permproof · cited by 10
- Module.Finite.of_quasiFiniteproof · cited by 7
- Finite.card_le_one_iff_subsingletonproof · cited by 6
- FirstOrder.Language.BoundedFormula.iInfproof · cited by 5
- Nat.card_funproof · cited by 5
- Nat.card_sumproof · cited by 5
- FintypeCat.fintypeproof · cited by 5
- Finite.card_eqproof · cited by 4
- hasStrictFDerivAt_list_prod'proof · cited by 4
- Subgroup.fintypeOfIndexNeZeroproof · cited by 4
- IsPGroup.card_modEq_card_fixedPointsproof · cited by 4
Showing the 200 most cited of 272.