Commit 2023-07-04 14:43 b0bb2972

View on Github →

chore: rename Fin.cast to Fin.castIso (#5584)

Estimated changes

deleted theorem Fin.addNat_cast
added theorem Fin.addNat_castIso
deleted def Fin.cast
deleted theorem Fin.castAdd_cast
added theorem Fin.castAdd_castIso
modified theorem Fin.castAdd_zero
added def Fin.castIso
added theorem Fin.castIso_addNat
added theorem Fin.castIso_castSucc
added theorem Fin.castIso_eq_cast
added theorem Fin.castIso_last
added theorem Fin.castIso_mk
added theorem Fin.castIso_natAdd
added theorem Fin.castIso_refl
added theorem Fin.castIso_succ_eq
added theorem Fin.castIso_to_equiv
added theorem Fin.castIso_trans
added theorem Fin.castIso_zero
deleted theorem Fin.cast_addNat
deleted theorem Fin.cast_addNat_left
deleted theorem Fin.cast_addNat_right
deleted theorem Fin.cast_addNat_zero
deleted theorem Fin.cast_castAdd_left
deleted theorem Fin.cast_castAdd_right
deleted theorem Fin.cast_castSucc
deleted theorem Fin.cast_eq_cast
deleted theorem Fin.cast_last
deleted theorem Fin.cast_mk
deleted theorem Fin.cast_natAdd
deleted theorem Fin.cast_natAdd_left
deleted theorem Fin.cast_natAdd_right
deleted theorem Fin.cast_natAdd_zero
deleted theorem Fin.cast_refl
deleted theorem Fin.cast_succ_eq
deleted theorem Fin.cast_to_equiv
deleted theorem Fin.cast_trans
deleted theorem Fin.cast_zero
deleted theorem Fin.coe_cast
added theorem Fin.coe_castIso
deleted theorem Fin.natAdd_cast
added theorem Fin.natAdd_castIso
deleted theorem Fin.natAdd_subNat_cast
modified theorem Fin.natAdd_zero
added theorem Fin.succ_castIso_eq
deleted theorem Fin.succ_cast_eq
deleted theorem Fin.symm_cast
added theorem Fin.symm_castIso
modified theorem Fin.repeat_add
modified theorem Fin.repeat_one
modified theorem List.get_ofFn