Commit 2024-04-07 17:47 b2af0d13

View on Github →

chore: Rename coe_nat/coe_int/coe_rat to natCast/intCast/ratCast (#11499) This is less exhaustive than its sibling #11486 because edge cases are harder to classify. No fundamental difficulty, just me being a bit fast and lazy. Reduce the diff of #11203

Estimated changes

deleted theorem WithBot.bot_ne_nat
added theorem WithBot.bot_ne_natCast
deleted theorem WithBot.coe_nat
added theorem WithBot.coe_natCast
added theorem WithBot.natCast_ne_bot
deleted theorem WithBot.nat_ne_bot
deleted theorem WithTop.coe_nat
added theorem WithTop.coe_natCast
added theorem WithTop.natCast_ne_top
deleted theorem WithTop.nat_ne_top
deleted theorem WithTop.top_ne_nat
added theorem WithTop.top_ne_natCast
deleted theorem Int.squarefree_coe_nat
added theorem Int.squarefree_natCast
deleted theorem Int.norm_coe_nat
added theorem Int.norm_natCast
deleted theorem Real.nnnorm_coe_nat
added theorem Real.nnnorm_natCast
deleted theorem Real.norm_coe_nat
added theorem Real.norm_natCast
deleted theorem Int.nnnorm_coe_nat
added theorem Int.nnnorm_natCast
deleted theorem ENNReal.coe_lt_coe_nat
added theorem ENNReal.coe_lt_natCast
deleted theorem ENNReal.coe_nat
added theorem ENNReal.coe_natCast
deleted theorem ENNReal.coe_nat_lt_coe
added theorem ENNReal.natCast_lt_coe
added theorem ENNReal.natCast_ne_top
deleted theorem ENNReal.nat_ne_top
deleted theorem ENNReal.ofReal_coe_nat
added theorem ENNReal.ofReal_natCast
deleted theorem ENNReal.top_ne_nat
added theorem ENNReal.top_ne_natCast
deleted theorem ENNReal.iSup_coe_nat
added theorem ENNReal.iSup_natCast
deleted theorem Int.coe_nat_pos
deleted theorem Int.coe_nat_succ_pos
added theorem Int.natCast_pos
added theorem Int.natCast_succ_pos
deleted theorem Pi.coe_int
added theorem Pi.intCast_apply
added theorem Pi.intCast_def
deleted theorem Pi.int_apply
deleted theorem NNRat.mk_coe_nat
added theorem NNRat.mk_natCast
deleted theorem Pi.coe_nat
added theorem Pi.natCast_apply
added theorem Pi.natCast_def
deleted theorem Pi.nat_apply
deleted theorem Rat.coe_int_div_eq_divInt
deleted theorem Rat.coe_int_eq_divInt
deleted theorem Rat.coe_nat_eq_divInt
added theorem Rat.intCast_eq_divInt
added theorem Rat.natCast_eq_divInt
deleted theorem Rat.coe_int_div
deleted theorem Rat.coe_int_div_self
deleted theorem Rat.coe_nat_div
deleted theorem Rat.coe_nat_div_self
added theorem Rat.intCast_div
added theorem Rat.intCast_div_self
deleted theorem Rat.inv_coe_int_den
deleted theorem Rat.inv_coe_int_num
deleted theorem Rat.inv_coe_nat_den
deleted theorem Rat.inv_coe_nat_num
added theorem Rat.inv_intCast_den
added theorem Rat.inv_intCast_num
added theorem Rat.inv_natCast_den
added theorem Rat.inv_natCast_num
added theorem Rat.natCast_div
added theorem Rat.natCast_div_self
deleted theorem NNReal.mk_coe_nat
added theorem NNReal.mk_natCast
deleted theorem SubfieldClass.coe_rat_mem
deleted theorem Matrix.zpow_neg_coe_nat
deleted theorem LucasLehmer.X.coe_nat
deleted theorem PadicInt.coe_int_eq
added theorem PadicInt.intCast_eq
deleted theorem Zsqrtd.coe_int_im
deleted theorem Zsqrtd.coe_int_re
deleted theorem Zsqrtd.coe_int_val
deleted theorem Zsqrtd.coe_nat_im
deleted theorem Zsqrtd.coe_nat_re
deleted theorem Zsqrtd.coe_nat_val
added theorem Zsqrtd.intCast_im
added theorem Zsqrtd.intCast_re
added theorem Zsqrtd.intCast_val
added theorem Zsqrtd.natCast_im
added theorem Zsqrtd.natCast_re
added theorem Zsqrtd.natCast_val
deleted theorem Zsqrtd.ofInt_eq_coe
deleted theorem Filter.Germ.coe_int
deleted theorem Filter.Germ.coe_nat
deleted theorem Derivation.map_coe_int
deleted theorem Derivation.map_coe_nat
added theorem Derivation.map_intCast
added theorem Derivation.map_natCast
deleted theorem selfZPow_coe_nat
added theorem selfZPow_natCast
deleted theorem selfZPow_neg_coe_nat
added theorem selfZPow_neg_natCast
deleted theorem selfZPow_sub_cast_nat
added theorem selfZPow_sub_natCast
deleted theorem coe_int_mem
added theorem intCast_mem
deleted theorem coe_nat_mem