mathlib documentation

data.fintype.fin

The structure of fintype (fin n) #

This file contains some basic results about the fintype instance for fin, especially properties of finset.univ : finset (fin n).

theorem fin.card_filter_univ_eq_vector_nth_eq_count {α : Type u_1} {n : } [decidable_eq α] (a : α) (v : vector α n) :