Theorems · Theorem · combinatorics
Fintype.complete
∀ {α : Type u_4} [self : Fintype α] (x : α), x ∈ Fintype.elemsA proof that elems contains every element of the type
- Defined in
- Mathlib.Data.Fintype.Defs
- Cited by
- 192 results in Mathlib
- Foundations
- Depth 54 from the axioms, rests on 808 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- Fintype
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- Fintypestatement and proof · cited by 7,736
- Fintype.elemsstatement · cited by 194
Cited by192
Results whose statement or proof uses this declaration.
- Finset.mem_univproof · cited by 361
- CategoryTheory.ComposableArrows.ext₁proof · cited by 16
- Height.mulHeight₁_eq_mulHeightproof · cited by 6
- Orientation.eq_or_eq_neg_of_isEmptyproof · cited by 6
- groupCohomology.comp_d₂₃_eqproof · cited by 5
- Complex.coe_basisOneIproof · cited by 5
- Orientation.areaForm_swapproof · cited by 5
- groupCohomology.cochainsMap_f_2_comp_cochainsIso₂proof · cited by 4
- Subgroup.strictPeriods_eq_zmultiples_one_of_T_memproof · cited by 4
- EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_affineIndependentproof · cited by 4
- SimplexCategory.mkOfSucc_δ_gtproof · cited by 4
- Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flatproof · cited by 4