Mathlib Map

Structures · Data types

Fintype

Fintype α means that α is finite, i.e. there are only finitely many distinct elements of type α. The evidence of this is a finset elems (a list up to permutation without duplicates), together with a proof that everything of type α is in the list.

Defined in
Mathlib.Data.Fintype.Defs
Shape
One type argument · adds elems, complete
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by3

Forgetful instances

Every Fintype is also a

Provided automatically by

Concrete types that are instances100

  • Bool
  • Quiver.Hom
  • TopCat.carrier
  • ZMod
  • CStarMatrix
  • Matrix
  • Units
  • Finsupp
  • CategoryTheory.Discrete
  • DFinsupp
  • TruncatedWittVector
  • LucasLehmer.X
  • CategoryTheory.PreZeroHypercover.I₀
  • Empty
  • Matrix.SpecialLinearGroup
  • PEmpty
  • AlgEquiv
  • AddChar
  • SimpleGraph
  • SignType
  • Hamming
  • Digraph
  • Abelianization
  • Polynomial.Gal
  • PontryaginDual
  • Sym2
  • ClassGroup
  • CategoryTheory.WithTerminal
  • CategoryTheory.WithInitial
  • AlgHom
  • LieModule.Weight
  • Sym
  • WithTopology
  • SimpleGraph.ConnectedComponent
  • Function.Embedding
  • ConjAct
  • SimpleGraph.Subgraph
  • Multiset.ToType
  • FirstOrder.Language.Symbols
  • CategoryTheory.Pairwise
  • OnePoint
  • CategoryTheory.Bicone
  • DihedralGroup
  • QuaternionGroup
  • CategoryTheory.Limits.limit
  • List.Vector
  • Finpartition
  • RelEmbedding
  • BoolAlg.carrier
  • AddEquiv
  • MulEquiv
  • NumberField.InfinitePlace
  • OrderedFinpartition
  • Nat.Partition
  • SimpleGraph.EdgeLabeling
  • RelHom
  • DirichletCharacter
  • LinOrd.carrier
  • SimpleGraph.Copy
  • DistLat.carrier
  • CategoryTheory.Limits.colimit
  • Ordering
  • PartOrd.carrier
  • CategoryTheory.Limits.WalkingParallelPair
  • CategoryTheory.Limits.WidePullbackShape
  • CategoryTheory.Limits.WidePushoutShape
  • Configuration.Dual
  • Composition
  • ConjClasses
  • CategoryTheory.Limits.WalkingMultispan
  • Computability.Γ'
  • Fin2
  • Symbol
  • CategoryTheory.Limits.WalkingPair
  • CompositionAsSet
  • Affine.Simplex.PointsWithCircumcenterIndex
  • CategoryTheory.Limits.WalkingMulticospan
  • Turing.PartrecToTM2.Γ'
  • CategoryTheory.Limits.WalkingParallelPairHom
  • SimpleGraph.Coloring
  • SimpleGraph.Dart
  • Module.End.Eigenvalues
  • Sym.Sym'
  • CategoryTheory.SimplicialObject.Splitting.IndexSet
  • Turing.TM2to1.Γ'
  • Module.Free.ChooseBasisIndex
  • CategoryTheory.Mat_.ι
  • SimpleGraph.Path
  • LTSeries
  • Subtype
  • Prod
  • OrderDual
  • Set.Elem
  • ULift
  • Fin
  • PUnit
  • Lex
  • HasQuotient.Quotient
  • Shrink
  • WithTop

How is a type an instance?

Loading the hierarchy index…

Assumed by8,462

Ancestors13