Def Fin.consCases

Modification history

2026-02-27 14:06

Mathlib/Data/Fin/Tuple/Basic.lean

chore(Data/Fin/Tuple/Basic): rename recursor arguments (#35703)

Modified Fin.consCases View on Github →

2023-01-17 13:37

Mathlib/Data/Fin/Tuple/Basic.lean

feat: port Data.Fin.Tuple.Basic (#1516)

Added Fin.consCases View on Github →