Commit 2023-07-13 01:24 906f7221

View on Github →

chore: bump to nightly-2023-07-01 (#5409)

Estimated changes

added theorem Fin.prod_univ_castSucc
deleted theorem Fin.prod_univ_castSuccEmb
modified theorem OfNat.ofNat_ne_one
modified theorem OfNat.ofNat_ne_zero
modified theorem OfNat.one_ne_ofNat
modified theorem OfNat.zero_ne_ofNat
modified theorem SimplexCategory.δ_comp_δ'
modified theorem Complex.im_ofNat
modified theorem Complex.ofReal_ofNat
modified theorem Complex.re_ofNat
deleted def Fin.addNat
added def Fin.addNatEmb
modified theorem Fin.addNat_mk
modified theorem Fin.addNat_one
modified theorem Fin.addNat_subNat
deleted def Fin.castAdd
added def Fin.castAddEmb
added theorem Fin.castIso_castSucc
deleted theorem Fin.castIso_castSuccEmb
modified theorem Fin.castIso_eq_cast
deleted def Fin.castLE
added def Fin.castLEEmb
deleted def Fin.castLT
added theorem Fin.castLT_castSucc
deleted theorem Fin.castLT_castSuccEmb
modified theorem Fin.castLT_succAbove
deleted def Fin.castPred
added theorem Fin.castPred_castSucc
deleted theorem Fin.castPred_castSuccEmb
deleted theorem Fin.castSuccEmb_castLT
deleted theorem Fin.castSuccEmb_castPred
deleted theorem Fin.castSuccEmb_fin_succ
deleted theorem Fin.castSuccEmb_inj
deleted theorem Fin.castSuccEmb_injective
deleted theorem Fin.castSuccEmb_lt_last
deleted theorem Fin.castSuccEmb_lt_succ
deleted theorem Fin.castSuccEmb_mk
deleted theorem Fin.castSuccEmb_one
deleted theorem Fin.castSuccEmb_pos
deleted theorem Fin.castSuccEmb_zero
added theorem Fin.castSucc_castLT
added theorem Fin.castSucc_castPred
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
deleted def Fin.clamp
modified theorem Fin.coeSucc_eq_succ
modified theorem Fin.coe_addNat
added theorem Fin.coe_castSucc
deleted theorem Fin.coe_castSuccEmb
added theorem Fin.coe_eq_castSucc
deleted theorem Fin.coe_eq_castSuccEmb
modified theorem Fin.coe_pred
deleted theorem Fin.exists_castSuccEmb_eq
added theorem Fin.exists_castSucc_eq
deleted theorem Fin.ext_iff
deleted def Fin.last
added theorem Fin.lastCases_castSucc
deleted theorem Fin.lastCases_castSuccEmb
deleted theorem Fin.le_castSuccEmb_iff
added theorem Fin.le_castSucc_iff
modified theorem Fin.le_coe_addNat
modified theorem Fin.lt_succ
modified theorem Fin.lt_succAbove_iff
deleted def Fin.natAdd
added def Fin.natAddEmb
added theorem Fin.natAdd_castSucc
deleted theorem Fin.natAdd_castSuccEmb
deleted def Fin.pred
deleted def Fin.predAbove
modified theorem Fin.predAbove_above
modified theorem Fin.predAbove_below
modified theorem Fin.predAbove_zero
deleted theorem Fin.pred_castSuccEmb_succ
added theorem Fin.pred_castSucc_succ
modified theorem Fin.pred_eq_iff_eq_succ
modified theorem Fin.pred_inj
modified theorem Fin.pred_le_pred_iff
modified theorem Fin.pred_lt_pred_iff
modified theorem Fin.pred_mk
modified theorem Fin.pred_one
modified theorem Fin.pred_succ
modified theorem Fin.pred_succAbove
modified theorem Fin.pred_succAbove_pred
added theorem Fin.range_castSucc
deleted theorem Fin.range_castSuccEmb
added theorem Fin.strictMono_addNat
added theorem Fin.strictMono_castAdd
added theorem Fin.strictMono_castLE
added theorem Fin.strictMono_natAdd
deleted def Fin.subNat
modified theorem Fin.subNat_addNat
deleted def Fin.succAbove
added def Fin.succAboveEmb
modified theorem Fin.succAbove_above
deleted theorem Fin.succAbove_aux
modified theorem Fin.succAbove_below
modified theorem Fin.succAbove_last
modified theorem Fin.succAbove_last_apply
modified theorem Fin.succAbove_lt_ge
modified theorem Fin.succAbove_lt_gt
modified theorem Fin.succAbove_lt_iff
modified theorem Fin.succAbove_pred
modified theorem Fin.succAbove_predAbove
modified theorem Fin.succAbove_zero
added theorem Fin.succ_castSucc
deleted theorem Fin.succ_castSuccEmb
modified theorem Fin.succ_pred
modified def Fin.init
modified def Fin.snoc
added theorem Fin.snoc_castSucc
deleted theorem Fin.snoc_castSuccEmb
modified theorem Fin.snoc_cast_add
added theorem Fin.snoc_comp_castSucc
deleted theorem Fin.snoc_comp_castSuccEmb
modified theorem Fin.snoc_update
added theorem Fin.image_castSucc
deleted theorem Fin.image_castSuccEmb
added theorem Fin.Iio_castSucc
deleted theorem Fin.Iio_castSuccEmb
modified theorem IsROrC.norm_ofNat
modified theorem IsROrC.ofNat_im
modified theorem IsROrC.ofNat_re
modified theorem IsROrC.ofReal_ofNat
modified theorem Polynomial.derivative_ofNat
modified theorem Polynomial.ofNat_comp
modified theorem ENNReal.coe_ofNat
deleted def String.isPrefixOf?
deleted def String.isSuffixOf
deleted def String.isSuffixOf?
deleted def String.stripPrefix
deleted def String.stripSuffix
modified theorem MultilinearMap.snoc_smul
modified theorem finSuccEquiv'_above
modified theorem finSuccEquiv'_below
modified theorem LucasLehmer.X.ofNat_fst
modified theorem LucasLehmer.X.ofNat_snd
modified theorem Zsqrtd.ofNat_im
modified theorem Zsqrtd.ofNat_re