Commit 2023-01-19 10:05 438cdc86

View on Github →

feat: introduce a new Fin.append and Fin.repeat (#1637) Port of https://github.com/leanprover-community/mathlib/pull/10346

Estimated changes

modified def Fin.append
added theorem Fin.append_assoc
added theorem Fin.append_elim0'
added theorem Fin.append_left
added theorem Fin.append_left_nil
added theorem Fin.append_right
added theorem Fin.append_right_nil
added theorem Fin.elim0'_append
deleted theorem Fin.fin_append_apply_zero
added theorem Fin.repeat_add
added theorem Fin.repeat_apply
added theorem Fin.repeat_one
added theorem Fin.repeat_succ
added theorem Fin.repeat_zero
added def Fin.«repeat»