Commit 2023-01-23 18:47 885e8510

View on Github →

feat: port Logic.Equiv.Fin (#1745)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.exists_castSucc_eq

added theorem Fin.val_lt_last

Created Mathlib/Logic/Equiv/Fin.lean

added def Equiv.piFinSucc

added def Equiv.piFinSuccAboveEquiv

added def Fin.castLeOrderIso

added theorem Fin.preimage_apply_01_prod'

added theorem Fin.preimage_apply_01_prod

added theorem Fin.snoc_eq_cons_rotate

added def OrderIso.finTwoArrowIso

added def OrderIso.piFinSuccAboveIso

added def OrderIso.piFinTwoIso

added theorem coe_finRotate

added theorem coe_finRotate_of_ne_last

added def finAddFlip

added theorem finAddFlip_apply_castAdd

added theorem finAddFlip_apply_mk_left

added theorem finAddFlip_apply_mk_right

added theorem finAddFlip_apply_natAdd

added def finCongr

added theorem finCongr_apply_coe

added theorem finCongr_apply_mk

added theorem finCongr_symm

added theorem finCongr_symm_apply_coe

added def finOneEquiv

added def finProdFinEquiv

added def finRotate

added theorem finRotate_apply_zero

added theorem finRotate_last'

added theorem finRotate_last

added theorem finRotate_of_lt

added theorem finRotate_one

added theorem finRotate_succ

added theorem finRotate_succ_apply

added theorem finRotate_zero

added def finSuccAboveEquiv

added theorem finSuccAboveEquiv_apply

added theorem finSuccAboveEquiv_symm_apply_last

added theorem finSuccAboveEquiv_symm_apply_ne_last

added def finSuccEquiv'

added theorem finSuccEquiv'_above

added theorem finSuccEquiv'_at

added theorem finSuccEquiv'_below

added theorem finSuccEquiv'_last_apply

added theorem finSuccEquiv'_last_apply_castSucc

added theorem finSuccEquiv'_ne_last_apply

added theorem finSuccEquiv'_succAbove

added theorem finSuccEquiv'_symm_coe_above

added theorem finSuccEquiv'_symm_coe_below

added theorem finSuccEquiv'_symm_none

added theorem finSuccEquiv'_symm_some

added theorem finSuccEquiv'_symm_some_above

added theorem finSuccEquiv'_symm_some_below

added theorem finSuccEquiv'_zero

added def finSuccEquiv

added def finSuccEquivLast

added theorem finSuccEquivLast_castSucc

added theorem finSuccEquivLast_last

added theorem finSuccEquivLast_symm_none

added theorem finSuccEquivLast_symm_some

added theorem finSuccEquiv_succ

added theorem finSuccEquiv_symm_none

added theorem finSuccEquiv_symm_some

added theorem finSuccEquiv_zero

added def finSumFinEquiv

added theorem finSumFinEquiv_apply_left

added theorem finSumFinEquiv_apply_right

added theorem finSumFinEquiv_symm_apply_castAdd

added theorem finSumFinEquiv_symm_apply_natAdd

added theorem finSumFinEquiv_symm_last

added def finTwoArrowEquiv

added def finTwoEquiv

added def finZeroEquiv'

added def finZeroEquiv

added def piFinTwoEquiv

added def prodEquivPiFinTwo