Def Fin.inductionOn

Modification history

2023-07-27 11:51

Mathlib/Data/Fin/Basic.lean

chore: bump to nightly-2023-07-15 (#5992) …

Deleted Fin.inductionOn View on Github →

2023-01-20 17:48

Mathlib/Data/Fin/Basic.lean

fix: make List.rec and Nat.rec computable (#1720) …

Added Fin.inductionOn View on Github →