Commit 2023-11-09 12:45 934bdf35

View on Github →

chore: add missing API around Fin.snoc (#8231) Adds a recursion principle for Fin n in terms of Fin.snoc and Fin.elim0, and a few related theorems

Estimated changes

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

added theorem Fin.append_cast_left

added theorem Fin.append_cast_right

added theorem Fin.append_left_snoc

added theorem Fin.append_right_cons

added theorem Fin.cons_eq_append

added def Fin.snocCases

added theorem Fin.snocCases_snoc

added def Fin.snocInduction

added theorem Fin.snoc_eq_append