Commit 2023-01-17 13:37 a43b3f18

View on Github →

feat: port Data.Fin.Tuple.Basic (#1516)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Fin/Basic.lean

Created Mathlib/Data/Fin/Tuple/Basic.lean

added def Fin.append

added theorem Fin.comp_cons

added theorem Fin.comp_init

added theorem Fin.comp_snoc

added theorem Fin.comp_tail

added def Fin.consCases

added def Fin.consInduction

added theorem Fin.cons_cases_cons

added theorem Fin.cons_eq_cons

added theorem Fin.cons_injective2

added theorem Fin.cons_injective_iff

added theorem Fin.cons_injective_of_injective

added theorem Fin.cons_le

added theorem Fin.cons_le_cons

added theorem Fin.cons_left_injective

added theorem Fin.cons_right_injective

added theorem Fin.cons_self_tail

added theorem Fin.cons_snoc_eq_snoc_cons

added theorem Fin.cons_succ

added theorem Fin.cons_update

added theorem Fin.cons_zero

added theorem Fin.eq_insertNth_iff

added theorem Fin.exists_fin_succ_pi

added theorem Fin.exists_fin_zero_pi

added theorem Fin.fin_append_apply_zero

added def Fin.find

added theorem Fin.find_eq_none_iff

added theorem Fin.find_eq_some_iff

added theorem Fin.find_min'

added theorem Fin.find_min

added theorem Fin.find_spec

added theorem Fin.forall_fin_succ_pi

added theorem Fin.forall_fin_zero_pi

added theorem Fin.forall_iff_succAbove

added def Fin.init

added theorem Fin.init_def

added theorem Fin.init_snoc

added theorem Fin.init_update_castSucc

added theorem Fin.init_update_last

added def Fin.insertNth

added theorem Fin.insertNth_add

added theorem Fin.insertNth_apply_above

added theorem Fin.insertNth_apply_below

added theorem Fin.insertNth_apply_same

added theorem Fin.insertNth_apply_succAbove

added theorem Fin.insertNth_binop

added theorem Fin.insertNth_comp_succAbove

added theorem Fin.insertNth_div

added theorem Fin.insertNth_eq_iff

added theorem Fin.insertNth_last'

added theorem Fin.insertNth_last

added theorem Fin.insertNth_le_iff

added theorem Fin.insertNth_mem_Icc

added theorem Fin.insertNth_mul

added theorem Fin.insertNth_sub

added theorem Fin.insertNth_sub_same

added theorem Fin.insertNth_zero'

added theorem Fin.insertNth_zero

added theorem Fin.insertNth_zero_right

added theorem Fin.isSome_find_iff

added theorem Fin.le_cons

added theorem Fin.le_insertNth_iff

added theorem Fin.mem_find_iff

added theorem Fin.mem_find_of_unique

added theorem Fin.nat_find_mem_find

added theorem Fin.pi_lex_lt_cons_cons

added theorem Fin.preimage_insertNth_Icc_of_mem

added theorem Fin.preimage_insertNth_Icc_of_not_mem

added theorem Fin.range_cons

added theorem Fin.range_fin_succ

added theorem Fin.sigma_eq_iff_eq_comp_cast

added theorem Fin.sigma_eq_of_eq_comp_cast

added def Fin.snoc

added theorem Fin.snoc_cast_add

added theorem Fin.snoc_cast_succ

added theorem Fin.snoc_comp_cast_add

added theorem Fin.snoc_comp_cast_succ

added theorem Fin.snoc_comp_nat_add

added theorem Fin.snoc_init_self

added theorem Fin.snoc_last

added theorem Fin.snoc_update

added def Fin.succAboveCases

added theorem Fin.succAbove_cases_eq_insertNth

added def Fin.tail

added theorem Fin.tail_cons

added theorem Fin.tail_def

added theorem Fin.tail_init_eq_init_tail

added theorem Fin.tail_update_succ

added theorem Fin.tail_update_zero

added theorem Fin.tuple0_le

added theorem Fin.update_cons_zero

added theorem Fin.update_snoc_last