Commit 2023-12-27 19:55 71bf2889

View on Github →

feat: add lemmas about Fin.rev (#8814)

Estimated changes

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.cast_eq_self

added theorem Fin.cast_rev

added theorem Fin.rev_succAbove

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

added theorem Fin.append_comp_rev

added theorem Fin.append_cons

added theorem Fin.append_rev

added theorem Fin.append_snoc

added theorem Fin.cons_comp_rev

added theorem Fin.cons_rev

added theorem Fin.insertNth_comp_rev

added theorem Fin.insertNth_rev

added theorem Fin.snoc_comp_rev

added theorem Fin.snoc_rev