Commit 2024-04-02 09:53 8d3a0438

View on Github →

refactor: Names the function of Equiv.piFinSuccAbove (#10545) Creates extractNth to do the opposite of insertNth for tuples. Rewrites the Equiv definition.

Estimated changes

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

added def Fin.extractNth

added theorem Fin.extractNth_insertNth

added theorem Fin.insertNth_extractNth

Modified Mathlib/Logic/Equiv/Fin.lean