Theorems · Inductive type · combinatorics

Fintype

Type u_4 → Type u_4

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

Cited by

7,736 results in Mathlib

Foundations

Depth 0 from the axioms, rests on 1 definitions · uses no axioms