Mathlib Map

Theorems · Definition · combinatorics

Fintype.elems

{α : Type u_4} → [self : Fintype α] → Finset α

The Finset containing all elements of a Fintype

Defined in
Mathlib.Data.Fintype.Defs
Cited by
194 results in Mathlib
Foundations
Depth 1 from the axioms, rests on 3 definitions · uses no axioms
Assumes
Fintype
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Finset.univ · cited by 3473Finset.univFintype.complete · cited by 192Fintype.completeCategoryTheory.ComposableArrows.ext₁ · cited by 16ComposableArrows.ext₁Height.mulHeight₁_eq_mulHeight · cited by 6Height.mulHeight₁_eq_mulH…Orientation.eq_or_eq_neg_of_isEmpty · cited by 6Orientation.eq_or_eq_neg_…groupCohomology.comp_d₂₃_eq · cited by 5groupCohomology.comp_d₂₃_…Complex.coe_basisOneI · cited by 5Complex.coe_basisOneIOrientation.areaForm_swap · cited by 5Orientation.areaForm_swapgroupCohomology.cochainsMap_f_2_comp_cochainsIso₂ · cited by 4groupCohomology.cochainsM…Subgroup.strictPeriods_eq_zmultiples_one_of_T_mem · cited by 4Subgroup.strictPeriods_eq…EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_affineIndependent · cited by 4EuclideanGeometry.oangle_…SimplexCategory.mkOfSucc_δ_gt · cited by 4SimplexCategory.mkOfSucc_…Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat · cited by 4LinearDisjoint.rank_inf_l…Orientation.areaForm_map · cited by 4Orientation.areaForm_mapMatrix.one_fin_two · cited by 3Matrix.one_fin_twoFinset · cited by 13712FinsetFintype · cited by 7736FintypeFintype.elemsCITED BYCITES

Cites2

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

Cited by196

Results whose statement or proof uses this declaration.