Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-14 15:22 299af47c

View on Github →

chore(data/fin/basic): move tuple stuff to a new file (#10295) There are almost 600 lines of tuple stuff, which is definitely sufficient to justify a standalone file. The author information has been guessed from the git history. Floris is responsible for cons and tail which came first in #1294, Chris added find, and Yury and Sébastien were involved all over the place. This is simply a cut-and-paste job, with the exception of the new module docstring which has been merged with the docstring for the tuple subheading.

Estimated changes

deleted def fin.append
deleted theorem fin.comp_cons
deleted theorem fin.comp_init
deleted theorem fin.comp_snoc
deleted theorem fin.comp_tail
deleted def fin.cons
deleted theorem fin.cons_le
deleted theorem fin.cons_self_tail
deleted theorem fin.cons_succ
deleted theorem fin.cons_update
deleted theorem fin.cons_zero
deleted theorem fin.eq_insert_nth_iff
deleted theorem fin.fin_append_apply_zero
deleted def fin.find
deleted theorem fin.find_eq_none_iff
deleted theorem fin.find_eq_some_iff
deleted theorem fin.find_min'
deleted theorem fin.find_min
deleted theorem fin.find_spec
deleted theorem fin.forall_iff_succ_above
deleted def fin.init
deleted theorem fin.init_def
deleted theorem fin.init_snoc
deleted theorem fin.init_update_cast_succ
deleted theorem fin.init_update_last
deleted def fin.insert_nth
deleted theorem fin.insert_nth_add
deleted theorem fin.insert_nth_apply_same
deleted theorem fin.insert_nth_binop
deleted theorem fin.insert_nth_div
deleted theorem fin.insert_nth_eq_iff
deleted theorem fin.insert_nth_last'
deleted theorem fin.insert_nth_last
deleted theorem fin.insert_nth_le_iff
deleted theorem fin.insert_nth_mem_Icc
deleted theorem fin.insert_nth_mul
deleted theorem fin.insert_nth_sub
deleted theorem fin.insert_nth_sub_same
deleted theorem fin.insert_nth_zero'
deleted theorem fin.insert_nth_zero
deleted theorem fin.insert_nth_zero_right
deleted theorem fin.is_some_find_iff
deleted theorem fin.le_cons
deleted theorem fin.le_insert_nth_iff
deleted theorem fin.mem_find_iff
deleted theorem fin.mem_find_of_unique
deleted theorem fin.nat_find_mem_find
deleted theorem fin.range_cons
deleted def fin.snoc
deleted theorem fin.snoc_cast_succ
deleted theorem fin.snoc_init_self
deleted theorem fin.snoc_last
deleted theorem fin.snoc_update
deleted def fin.tail
deleted theorem fin.tail_cons
deleted theorem fin.tail_def
deleted theorem fin.tail_update_succ
deleted theorem fin.tail_update_zero
deleted theorem fin.tuple0_le
deleted theorem fin.update_cons_zero
deleted theorem fin.update_snoc_last
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.cons
added theorem fin.cons_le
added theorem fin.cons_self_tail
added theorem fin.cons_succ
added theorem fin.cons_update
added theorem fin.cons_zero
added theorem fin.eq_insert_nth_iff
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 def fin.init
added theorem fin.init_def
added theorem fin.init_snoc
added theorem fin.init_update_last
added def fin.insert_nth
added theorem fin.insert_nth_add
added theorem fin.insert_nth_binop
added theorem fin.insert_nth_div
added theorem fin.insert_nth_eq_iff
added theorem fin.insert_nth_last'
added theorem fin.insert_nth_last
added theorem fin.insert_nth_le_iff
added theorem fin.insert_nth_mem_Icc
added theorem fin.insert_nth_mul
added theorem fin.insert_nth_sub
added theorem fin.insert_nth_zero'
added theorem fin.insert_nth_zero
added theorem fin.is_some_find_iff
added theorem fin.le_cons
added theorem fin.le_insert_nth_iff
added theorem fin.mem_find_iff
added theorem fin.mem_find_of_unique
added theorem fin.nat_find_mem_find
added theorem fin.range_cons
added def fin.snoc
added theorem fin.snoc_cast_succ
added theorem fin.snoc_init_self
added theorem fin.snoc_last
added theorem fin.snoc_update
added def fin.tail
added theorem fin.tail_cons
added theorem fin.tail_def
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