Theorems · Theorem · combinatorics
nonempty_fintype
∀ (α : Type u_4) [Finite α], Nonempty (Fintype α)
See also nonempty_encodable, nonempty_denumerable.
- Defined in
- Mathlib.Data.Fintype.Basic
- Cited by
- 261 results in Mathlib
- Foundations
- Depth 59 from the axioms, rests on 941 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- Finite
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivproof · cited by 8,337
- Fintypestatement · cited by 7,736
- Equiv.symmproof · cited by 3,681
- Finitestatement and proof · cited by 3,029
- Finite.exists_equiv_finproof · cited by 23
- Fintype.ofEquivproof · cited by 15
Cited by262
Results whose statement or proof uses this declaration.
- Fintype.ofFiniteproof · cited by 255
- Module.Finite.of_basisproof · cited by 22
- Finite.induction_empty_optionproof · cited by 10
- Equiv.Perm.cycle_induction_onproof · cited by 8
- LinearMap.BilinForm.dualSubmodule_span_of_basisproof · cited by 7
- rank_piproof · cited by 6
- Algebra.IsInvariant.isIntegralproof · cited by 6
- Equiv.Perm.swap_induction_onproof · cited by 5
- ZSpan.isAddFundamentalDomainproof · cited by 5
- Subgroup.index_ne_zero_of_finiteproof · cited by 5
- MultilinearMap.ext_ringproof · cited by 5
- Algebra.IsInvariant.exists_smul_of_under_eqproof · cited by 5
Showing the 200 most cited of 262.