mathlib3 documentation

data.fintype.fin

The structure of fintype (fin n) #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) :