Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-18 02:10 2d00f208

View on Github →

feat(data/fin): init and snoc (#1978)

  • feat(data/fin): append
  • Update fin.lean
  • Update fintype.lean
  • replace but_last with init
  • cons and append commute
  • change append to snoc
  • comp_snoc and friends
  • markdown in docstrings
  • fix docstring

Estimated changes

added theorem fin.cast_succ_fin_succ
added theorem fin.comp_cons
added theorem fin.comp_init
added theorem fin.comp_snoc
added theorem fin.comp_tail
added theorem fin.eq_last_of_not_lt
added def fin.init
added theorem fin.init_snoc
added theorem fin.init_update_last
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 theorem fin.succ_last
added theorem fin.update_snoc_last
added theorem fin.sum_univ_cast_succ
added theorem fin.univ_cast_succ
added theorem function.comp_update