Commit 2024-02-12 22:42 839d7c02

View on Github →

feat: Fin.exists_fin_succ' (#10459) Adds Fin.exists_fin_succ', which is analogous to Fin.forall_fin_succ'.

Estimated changes

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.exists_fin_succ'