Commit 2024-06-06 10:40 6a712475

View on Github →

feat: define Fin2.rev analogously to Fin.rev (#10818) This defines Fin2.rev, the mapping from i : Fin2 to (morally) last - i, and proves it's an involution.

Estimated changes

Modified Mathlib/Data/Fin/Fin2.lean

added def Fin2.castSucc

added def Fin2.last

added def Fin2.rev

added theorem Fin2.rev_castSucc

added theorem Fin2.rev_involutive

added theorem Fin2.rev_last

added theorem Fin2.rev_rev