Commit 2023-01-12 19:47 a941ebfd

View on Github →

feat: port Data.Fin.Basic (#1084) mathlib3 SHA: 0bd2ea37bcba5769e14866170f251c9bc64e35d7

Estimated changes

added theorem Nat.Up.WF
added theorem Nat.Up.next
added def Nat.Up
added def Nat.upRel
added def Fin.addCases
added theorem Fin.addCases_left
added theorem Fin.addCases_right
added def Fin.addNat
added theorem Fin.addNat_cast
added theorem Fin.addNat_mk
added theorem Fin.addNat_one
added theorem Fin.addNat_subNat
deleted def Fin.addOverflows?
modified theorem Fin.add_def
added theorem Fin.add_one_le_iff
added theorem Fin.add_one_lt_iff
added theorem Fin.add_one_pos
added theorem Fin.bot_eq_zero
added theorem Fin.cases_succ'
added theorem Fin.cases_succ
added theorem Fin.cases_zero
added def Fin.cast
added def Fin.castAdd
added theorem Fin.castAdd_cast
added theorem Fin.castAdd_castAdd
added theorem Fin.castAdd_castLt
added theorem Fin.castAdd_lt
added theorem Fin.castAdd_mk
added theorem Fin.castAdd_natAdd
added theorem Fin.castAdd_zero
added def Fin.castLe
added theorem Fin.castLe_castLe
added theorem Fin.castLe_comp_castLe
added theorem Fin.castLe_mk
added theorem Fin.castLe_of_eq
added theorem Fin.castLe_succ
added theorem Fin.castLe_zero
added def Fin.castLt
added theorem Fin.castLt_castAdd
added theorem Fin.castLt_mk
added theorem Fin.castLt_succAbove
added def Fin.castPred
added theorem Fin.castPred_castSucc
added theorem Fin.castPred_last
added theorem Fin.castPred_mk'
added theorem Fin.castPred_mk
added theorem Fin.castPred_monotone
added theorem Fin.castPred_one
added theorem Fin.castPred_zero
added def Fin.castSucc
added theorem Fin.castSucc_castPred
added theorem Fin.castSucc_cast_lt
added theorem Fin.castSucc_fin_succ
added theorem Fin.castSucc_inj
added theorem Fin.castSucc_injective
added theorem Fin.castSucc_lt_last
added theorem Fin.castSucc_lt_succ
added theorem Fin.castSucc_mk
added theorem Fin.castSucc_one
added theorem Fin.castSucc_pos
added theorem Fin.castSucc_zero
added theorem Fin.cast_addNat
added theorem Fin.cast_addNat_left
added theorem Fin.cast_addNat_right
added theorem Fin.cast_addNat_zero
added theorem Fin.cast_castAdd_left
added theorem Fin.cast_castAdd_right
added theorem Fin.cast_castSucc
added theorem Fin.cast_eq_cast
added theorem Fin.cast_last
added theorem Fin.cast_lt_castSucc
added theorem Fin.cast_mk
added theorem Fin.cast_natAdd
added theorem Fin.cast_natAdd_left
added theorem Fin.cast_natAdd_right
added theorem Fin.cast_natAdd_zero
added theorem Fin.cast_nat_eq_last
added theorem Fin.cast_refl
added theorem Fin.cast_succ_eq
added theorem Fin.cast_to_equiv
added theorem Fin.cast_trans
added theorem Fin.cast_val_eq_self
added theorem Fin.cast_zero
deleted def Fin.checkedAdd
deleted def Fin.checkedMul
deleted def Fin.checkedSub
deleted theorem Fin.checked_add_spec
deleted theorem Fin.checked_mul_spec
deleted theorem Fin.checked_sub_spec
added def Fin.clamp
added theorem Fin.coeSucc_eq_succ
added theorem Fin.coe_addNat
added theorem Fin.coe_cast
added theorem Fin.coe_castAdd
added theorem Fin.coe_castLe
added theorem Fin.coe_castLt
added theorem Fin.coe_castPred
added theorem Fin.coe_castSucc
added theorem Fin.coe_clamp
added theorem Fin.coe_divNat
added theorem Fin.coe_eq_castSucc
added theorem Fin.coe_fin_one
added theorem Fin.coe_modNat
added theorem Fin.coe_mul
added theorem Fin.coe_natAdd
added theorem Fin.coe_neg_one
added theorem Fin.coe_ofNat_eq_mod'
added theorem Fin.coe_of_nat_eq_mod
added theorem Fin.coe_orderIso_apply
added theorem Fin.coe_pred
added theorem Fin.coe_subNat
added theorem Fin.coe_sub_iff_le
added theorem Fin.coe_sub_iff_lt
added theorem Fin.coe_sub_one
added def Fin.divNat
added def Fin.elim0'
added theorem Fin.eq_iff_veq
added theorem Fin.eq_last_of_not_lt
added theorem Fin.eq_mk_iff_val_eq
added theorem Fin.eq_succ_of_ne_zero
added theorem Fin.eq_zero_or_eq_succ
added def Fin.equivSubtype
added theorem Fin.exists_fin_one
added theorem Fin.exists_fin_succ
added theorem Fin.exists_fin_two
added theorem Fin.exists_iff
added theorem Fin.exists_succ_eq_iff
modified theorem Fin.ext
modified theorem Fin.ext_iff
added theorem Fin.fin_one_eq_zero
added theorem Fin.forall_fin_one
added theorem Fin.forall_fin_succ
added theorem Fin.forall_fin_two
added theorem Fin.forall_iff
deleted theorem Fin.gt_wf
added theorem Fin.induction_succ
added theorem Fin.induction_zero
added theorem Fin.is_le'
added theorem Fin.is_le
added theorem Fin.is_lt
added def Fin.last
added def Fin.lastCases
added theorem Fin.lastCases_castSucc
added theorem Fin.lastCases_last
added theorem Fin.last_add_one
added theorem Fin.last_le_iff
added theorem Fin.last_pos
added theorem Fin.last_sub
deleted theorem Fin.le_antisymm
added theorem Fin.le_castSucc_iff
added theorem Fin.le_coe_addNat
added theorem Fin.le_coe_natAdd
added theorem Fin.le_iff_val_le_val
added theorem Fin.le_last
deleted theorem Fin.le_refl
added theorem Fin.le_sub_one_iff
deleted theorem Fin.le_total
deleted theorem Fin.le_trans
added theorem Fin.le_val_last
added theorem Fin.le_zero_iff
added theorem Fin.lift_fun_iff_succ
added theorem Fin.lt_add_one_iff
deleted theorem Fin.lt_iff_le_not_le
added theorem Fin.lt_iff_val_lt_val
added theorem Fin.lt_sub_one_iff
added theorem Fin.lt_succ
added theorem Fin.lt_succAbove_iff
added theorem Fin.max_val
added theorem Fin.min_val
added theorem Fin.mk_bit0
added theorem Fin.mk_bit1
added theorem Fin.mk_eq_mk
added theorem Fin.mk_le_mk
added theorem Fin.mk_le_of_le_val
added theorem Fin.mk_lt_mk
added theorem Fin.mk_lt_of_lt_val
added theorem Fin.mk_one
added theorem Fin.mk_succ_pos
added theorem Fin.mk_val
added theorem Fin.mk_zero
added def Fin.modNat
modified theorem Fin.mod_def
deleted theorem Fin.mod_eq_of_lt
deleted theorem Fin.mod_lt
deleted def Fin.mulOverflows?
modified theorem Fin.mul_def
added def Fin.natAdd
added theorem Fin.natAdd_cast
added theorem Fin.natAdd_castAdd
added theorem Fin.natAdd_castSucc
added theorem Fin.natAdd_last
added theorem Fin.natAdd_mk
added theorem Fin.natAdd_natAdd
added theorem Fin.natAdd_subNat_cast
added theorem Fin.natAdd_zero
added theorem Fin.ne_iff_vne
deleted theorem Fin.neg_def
added theorem Fin.not_lt_zero
deleted def Fin.ofInt'
added def Fin.ofNat''
modified theorem Fin.ofNat'_one
deleted theorem Fin.ofNat'_succ
modified theorem Fin.ofNat'_zero
added theorem Fin.ofNat_eq_val
deleted theorem Fin.one_def
added theorem Fin.one_eq_zero_iff
added theorem Fin.one_lt_succ_succ
added theorem Fin.one_pos
added theorem Fin.one_succAbove_one
added theorem Fin.one_succAbove_succ
added theorem Fin.one_succAbove_zero
deleted theorem Fin.one_val
added theorem Fin.orderEmbedding_eq
deleted def Fin.overflowingAdd
deleted def Fin.overflowingMul
added theorem Fin.pos_iff_ne_zero
added theorem Fin.pos_iff_nonempty
added def Fin.pred
added def Fin.predAbove
added theorem Fin.predAbove_above
added theorem Fin.predAbove_below
added theorem Fin.predAbove_last
added theorem Fin.predAbove_zero
added theorem Fin.pred_add_one
added theorem Fin.pred_castSucc_succ
added theorem Fin.pred_inj
added theorem Fin.pred_le_pred_iff
added theorem Fin.pred_lt_pred_iff
added theorem Fin.pred_mk
added theorem Fin.pred_mk_succ'
added theorem Fin.pred_mk_succ
added theorem Fin.pred_one
added theorem Fin.pred_succ
added theorem Fin.pred_succAbove
added theorem Fin.range_castLe
added theorem Fin.range_castSucc
added theorem Fin.range_succ
added theorem Fin.range_succAbove
added def Fin.rev
added def Fin.revOrderIso
added theorem Fin.rev_bijective
added theorem Fin.rev_eq
added theorem Fin.rev_inj
added theorem Fin.rev_injective
added theorem Fin.rev_involutive
added theorem Fin.rev_le_rev
added theorem Fin.rev_lt_rev
added theorem Fin.rev_rev
added theorem Fin.rev_surjective
added theorem Fin.rev_symm
modified theorem Fin.size_positive'
modified theorem Fin.size_positive
added theorem Fin.strictMono_unique
added def Fin.subNat
added theorem Fin.subNat_addNat
added theorem Fin.subNat_mk
deleted def Fin.subUnderflows?
modified theorem Fin.sub_def
added theorem Fin.sub_one_lt_iff
added def Fin.succAbove
added theorem Fin.succAbove_above
added theorem Fin.succAbove_aux
added theorem Fin.succAbove_below
added theorem Fin.succAbove_castLt
added theorem Fin.succAbove_last
added theorem Fin.succAbove_left_inj
added theorem Fin.succAbove_lt_ge
added theorem Fin.succAbove_lt_gt
added theorem Fin.succAbove_lt_iff
added theorem Fin.succAbove_ne
added theorem Fin.succAbove_ne_zero
added theorem Fin.succAbove_pos
added theorem Fin.succAbove_pred
added theorem Fin.succAbove_zero
added def Fin.succRec
added def Fin.succRecOn
added theorem Fin.succRecOn_succ
added theorem Fin.succRecOn_zero
added theorem Fin.succ_castSucc
added theorem Fin.succ_cast_eq
added theorem Fin.succ_eq_last_succ
added theorem Fin.succ_inj
added theorem Fin.succ_injective
added theorem Fin.succ_last
added theorem Fin.succ_le_succ_iff
added theorem Fin.succ_lt_succ_iff
added theorem Fin.succ_mk
added theorem Fin.succ_ne_zero
added theorem Fin.succ_one_eq_two'
added theorem Fin.succ_one_eq_two
added theorem Fin.succ_pos
added theorem Fin.succ_pred
added theorem Fin.succ_succAbove_one
added theorem Fin.succ_succ_ne_one
added theorem Fin.succ_zero_eq_one'
added theorem Fin.succ_zero_eq_one
added theorem Fin.symm_cast
added theorem Fin.top_eq_last
deleted def Fin.underflowingSub
deleted def Fin.upRel
added def Fin.valEmbedding
added theorem Fin.val_add
added theorem Fin.val_add_eq_ite
added theorem Fin.val_add_one
added theorem Fin.val_add_one_of_lt
added theorem Fin.val_bit0
added theorem Fin.val_bit1
added theorem Fin.val_cast_of_lt
deleted theorem Fin.val_eq_of_lt
added theorem Fin.val_eq_val
added theorem Fin.val_fin_le
added theorem Fin.val_fin_lt
added theorem Fin.val_injective
added theorem Fin.val_last
added theorem Fin.val_mk
added theorem Fin.val_mul
added theorem Fin.val_one''
added theorem Fin.val_one'
added theorem Fin.val_one
added theorem Fin.val_rev
added theorem Fin.val_strictMono
added theorem Fin.val_succ
added theorem Fin.val_succEmbedding
added theorem Fin.val_two
added theorem Fin.val_zero
deleted theorem Fin.zero_def
added theorem Fin.zero_eq_one_iff
added theorem Fin.zero_le
added theorem Fin.zero_lt_one
added theorem Fin.zero_ne_one
added theorem Fin.zero_succAbove
deleted theorem Nat.Up.WF
deleted theorem Nat.Up.next
deleted def Nat.Up
deleted def Nat.upRel
added def finZeroElim
deleted theorem zero_lt_of_lt
deleted theorem UInt16.size_positive
modified theorem UInt16.val_eq_of_lt
deleted theorem UInt32.size_positive
modified theorem UInt32.val_eq_of_lt
deleted theorem UInt64.size_positive
modified theorem UInt64.val_eq_of_lt
deleted theorem UInt8.size_positive
modified theorem UInt8.val_eq_of_lt
deleted theorem USize.size_positive
modified theorem USize.val_eq_of_lt
added def Fin.ofInt'