Commit 2023-01-26 13:08 99d24015

View on Github →

feat: port Data.Fintype.Fin (#1847)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Fintype/Fin.lean

added theorem Fin.Ioi_succ

added theorem Fin.Ioi_zero_eq_map

added theorem Fin.card_filter_univ_eq_vector_get_eq_count

added theorem Fin.card_filter_univ_succ'

added theorem Fin.card_filter_univ_succ