Commit 2024-04-17 11:15 145460b9

View on Github →

chore: Rename nat_cast/int_cast/rat_cast to natCast/intCast/ratCast (#11486) Now that I am defining NNRat.cast, I want a definitive answer to this naming issue. Plenty of lemmas in mathlib already use natCast/intCast/ratCast over nat_cast/int_cast/rat_cast, and this matches with the general expectation that underscore-separated name parts correspond to a single declaration.

Estimated changes

added theorem frobenius_natCast
deleted theorem frobenius_nat_cast
deleted theorem Function.support_nat_cast
added theorem inv_intCast_smul_comm
added theorem inv_intCast_smul_eq
deleted theorem inv_int_cast_smul_comm
deleted theorem inv_int_cast_smul_eq
added theorem inv_natCast_smul_comm
added theorem inv_natCast_smul_eq
deleted theorem inv_nat_cast_smul_comm
deleted theorem inv_nat_cast_smul_eq
added theorem map_intCast_smul
deleted theorem map_int_cast_smul
added theorem map_inv_intCast_smul
deleted theorem map_inv_int_cast_smul
added theorem map_inv_natCast_smul
deleted theorem map_inv_nat_cast_smul
added theorem map_natCast_smul
deleted theorem map_nat_cast_smul
added theorem map_ratCast_smul
deleted theorem map_rat_cast_smul
added theorem ratCast_smul_eq
deleted theorem rat_cast_smul_eq
added theorem Nonneg.mk_natCast
deleted theorem Nonneg.mk_nat_cast
added theorem iUnion_Icc_add_intCast
deleted theorem iUnion_Icc_add_int_cast
added theorem iUnion_Icc_intCast
deleted theorem iUnion_Icc_int_cast
added theorem iUnion_Ico_add_intCast
deleted theorem iUnion_Ico_add_int_cast
added theorem iUnion_Ico_intCast
deleted theorem iUnion_Ico_int_cast
added theorem iUnion_Ioc_add_intCast
deleted theorem iUnion_Ioc_add_int_cast
added theorem iUnion_Ioc_intCast
deleted theorem iUnion_Ioc_int_cast
deleted theorem Polynomial.aeval_nat_cast
deleted theorem Polynomial.C_eq_int_cast
deleted theorem Polynomial.C_eq_nat_cast
added theorem Polynomial.natCast_mul
deleted theorem Polynomial.nat_cast_mul
added theorem Polynomial.intCast_inj
deleted theorem Polynomial.int_cast_inj
added theorem Polynomial.natCast_inj
deleted theorem Polynomial.nat_cast_inj
deleted theorem Polynomial.eval_int_cast
deleted theorem Polynomial.eval_nat_cast
deleted theorem Polynomial.map_int_cast
deleted theorem Polynomial.nat_cast_comp
added theorem Quaternion.coe_intCast
deleted theorem Quaternion.coe_int_cast
added theorem Quaternion.coe_natCast
deleted theorem Quaternion.coe_nat_cast
added theorem Quaternion.coe_ratCast
deleted theorem Quaternion.coe_rat_cast
added theorem Quaternion.intCast_im
added theorem Quaternion.intCast_imI
added theorem Quaternion.intCast_imJ
added theorem Quaternion.intCast_imK
added theorem Quaternion.intCast_re
deleted theorem Quaternion.int_cast_im
deleted theorem Quaternion.int_cast_imI
deleted theorem Quaternion.int_cast_imJ
deleted theorem Quaternion.int_cast_imK
deleted theorem Quaternion.int_cast_re
added theorem Quaternion.natCast_im
added theorem Quaternion.natCast_imI
added theorem Quaternion.natCast_imJ
added theorem Quaternion.natCast_imK
added theorem Quaternion.natCast_re
deleted theorem Quaternion.nat_cast_im
deleted theorem Quaternion.nat_cast_imI
deleted theorem Quaternion.nat_cast_imJ
deleted theorem Quaternion.nat_cast_imK
deleted theorem Quaternion.nat_cast_re
added theorem Quaternion.ratCast_im
added theorem Quaternion.ratCast_imI
added theorem Quaternion.ratCast_imJ
added theorem Quaternion.ratCast_imK
added theorem Quaternion.ratCast_re
deleted theorem Quaternion.rat_cast_im
deleted theorem Quaternion.rat_cast_imI
deleted theorem Quaternion.rat_cast_imJ
deleted theorem Quaternion.rat_cast_imK
deleted theorem Quaternion.rat_cast_re
deleted theorem CentroidHom.coe_int_cast
deleted theorem CentroidHom.coe_nat_cast
added theorem star_intCast_smul
deleted theorem star_int_cast_smul
added theorem star_inv_intCast_smul
deleted theorem star_inv_int_cast_smul
added theorem star_inv_natCast_smul
deleted theorem star_inv_nat_cast_smul
added theorem star_natCast_smul
deleted theorem star_nat_cast_smul
added theorem star_ratCast_smul
deleted theorem star_rat_cast_smul
added theorem intCast_memℓp_infty
deleted theorem int_cast_memℓp_infty
added theorem lp.infty_coeFn_intCast
deleted theorem lp.infty_coeFn_int_cast
added theorem lp.infty_coeFn_natCast
deleted theorem lp.infty_coeFn_nat_cast
added theorem natCast_memℓp_infty
deleted theorem nat_cast_memℓp_infty
modified theorem Complex.natCast_log
added theorem Real.ceil_logb_natCast
deleted theorem Real.ceil_logb_nat_cast
deleted theorem Real.floor_logb_nat_cast
deleted theorem Real.log_int_cast_nonneg
deleted theorem Real.log_nat_cast_nonneg
added theorem Complex.cpow_intCast
deleted theorem Complex.cpow_int_cast
added theorem Complex.cpow_natCast
deleted theorem Complex.cpow_nat_cast
added theorem ENNReal.rpow_intCast
deleted theorem ENNReal.rpow_int_cast
added theorem ENNReal.rpow_natCast
deleted theorem ENNReal.rpow_nat_cast
added theorem NNReal.rpow_natCast
deleted theorem NNReal.rpow_nat_cast
modified theorem Real.exp_one_pow
added theorem Real.rpow_intCast
deleted theorem Real.rpow_int_cast
added theorem Real.rpow_natCast
deleted theorem Real.rpow_nat_cast
modified theorem Complex.abs_intCast
added theorem Complex.conj_natCast
deleted theorem Complex.conj_nat_cast
added theorem Complex.div_intCast
added theorem Complex.div_intCast_im
added theorem Complex.div_intCast_re
deleted theorem Complex.div_int_cast
deleted theorem Complex.div_int_cast_im
deleted theorem Complex.div_int_cast_re
added theorem Complex.div_natCast
added theorem Complex.div_natCast_im
added theorem Complex.div_natCast_re
deleted theorem Complex.div_nat_cast
deleted theorem Complex.div_nat_cast_im
deleted theorem Complex.div_nat_cast_re
added theorem Complex.div_ratCast
added theorem Complex.div_ratCast_im
added theorem Complex.div_ratCast_re
deleted theorem Complex.div_rat_cast
deleted theorem Complex.div_rat_cast_im
deleted theorem Complex.div_rat_cast_re
added theorem Complex.intCast_im
added theorem Complex.intCast_re
deleted theorem Complex.int_cast_im
deleted theorem Complex.int_cast_re
added theorem Complex.natCast_im
added theorem Complex.natCast_re
deleted theorem Complex.nat_cast_im
deleted theorem Complex.nat_cast_re
added theorem Complex.normSq_intCast
deleted theorem Complex.normSq_int_cast
added theorem Complex.normSq_natCast
deleted theorem Complex.normSq_nat_cast
added theorem Complex.normSq_ratCast
deleted theorem Complex.normSq_rat_cast
added theorem Complex.ofReal_intCast
deleted theorem Complex.ofReal_int_cast
added theorem Complex.ofReal_natCast
deleted theorem Complex.ofReal_nat_cast
added theorem Complex.ofReal_ratCast
deleted theorem Complex.ofReal_rat_cast
added theorem Complex.ratCast_im
added theorem Complex.ratCast_re
deleted theorem Complex.rat_cast_im
deleted theorem Complex.rat_cast_re
added theorem ENNReal.natCast_sub
deleted theorem ENNReal.nat_cast_sub
added theorem Fin.natCast_eq_zero
added theorem Fin.natCast_self
deleted theorem Fin.nat_cast_eq_zero
deleted theorem Fin.nat_cast_self
added theorem Fin.neg_natCast_eq_one
deleted theorem Fin.neg_nat_cast_eq_one
added theorem Fin.val_natCast
deleted theorem Fin.val_nat_cast
deleted theorem Function.support_int_cast
added theorem Num.of_natCast
deleted theorem Num.of_nat_cast
added theorem ZNum.of_intCast
deleted theorem ZNum.of_int_cast
added theorem ZNum.of_natCast
deleted theorem ZNum.of_nat_cast
deleted theorem Real.nat_cast_le_toNNReal
deleted theorem Real.nat_cast_lt_toNNReal
deleted theorem Real.toNNReal_eq_nat_cast
deleted theorem Real.toNNReal_le_nat_cast
deleted theorem Real.toNNReal_lt_nat_cast
added theorem Real.sign_intCast
deleted theorem Real.sign_int_cast
added theorem ZMod.cast_intCast'
added theorem ZMod.cast_intCast
deleted theorem ZMod.cast_int_cast'
deleted theorem ZMod.cast_int_cast
added theorem ZMod.cast_natCast'
added theorem ZMod.cast_natCast
deleted theorem ZMod.cast_nat_cast'
deleted theorem ZMod.cast_nat_cast
added theorem ZMod.coe_intCast
deleted theorem ZMod.coe_int_cast
added theorem ZMod.intCast_cast
added theorem ZMod.intCast_comp_cast
added theorem ZMod.intCast_mod
added theorem ZMod.intCast_zmod_cast
deleted theorem ZMod.int_cast_cast
deleted theorem ZMod.int_cast_comp_cast
deleted theorem ZMod.int_cast_mod
deleted theorem ZMod.int_cast_surjective
deleted theorem ZMod.int_cast_zmod_cast
added theorem ZMod.ker_intCastAddHom
deleted theorem ZMod.ker_int_castAddHom
deleted theorem ZMod.ker_int_castRingHom
added theorem ZMod.natCast_comp_val
added theorem ZMod.natCast_mod
added theorem ZMod.natCast_self'
added theorem ZMod.natCast_self
added theorem ZMod.natCast_toNat
added theorem ZMod.natCast_val
added theorem ZMod.natCast_zmod_val
deleted theorem ZMod.nat_cast_comp_val
deleted theorem ZMod.nat_cast_mod
deleted theorem ZMod.nat_cast_self'
deleted theorem ZMod.nat_cast_self
deleted theorem ZMod.nat_cast_toNat
deleted theorem ZMod.nat_cast_val
deleted theorem ZMod.nat_cast_zmod_val
added theorem ZMod.val_intCast
deleted theorem ZMod.val_int_cast
added theorem ZMod.val_natCast
added theorem ZMod.val_natCast_of_lt
deleted theorem ZMod.val_nat_cast
deleted theorem ZMod.val_nat_cast_of_lt
added theorem PerfectClosure.intCast
deleted theorem PerfectClosure.int_cast
added theorem PerfectClosure.natCast
deleted theorem PerfectClosure.nat_cast
modified theorem ZMod.χ₄_nat_mod_four
modified theorem ZMod.χ₈_nat_mod_eight
added theorem PadicInt.coe_intCast
deleted theorem PadicInt.coe_int_cast
added theorem PadicInt.coe_natCast
deleted theorem PadicInt.coe_nat_cast
added theorem Zsqrtd.norm_intCast
deleted theorem Zsqrtd.norm_int_cast
added theorem Zsqrtd.norm_natCast
deleted theorem Zsqrtd.norm_nat_cast
added theorem Ring.choose_natCast
deleted theorem Ring.choose_nat_cast
added theorem RingCon.coe_intCast
deleted theorem RingCon.coe_int_cast
added theorem RingCon.coe_natCast
deleted theorem RingCon.coe_nat_cast
deleted theorem Localization.mk_int_cast
deleted theorem Localization.mk_nat_cast
added theorem Ordinal.lift_natCast
deleted theorem Ordinal.lift_nat_cast
added theorem Ordinal.natCast_div
added theorem Ordinal.natCast_inj
added theorem Ordinal.natCast_le
added theorem Ordinal.natCast_lt
added theorem Ordinal.natCast_mod
added theorem Ordinal.natCast_mul
added theorem Ordinal.natCast_pos
added theorem Ordinal.natCast_sub
deleted theorem Ordinal.nat_cast_div
deleted theorem Ordinal.nat_cast_eq_zero
deleted theorem Ordinal.nat_cast_inj
deleted theorem Ordinal.nat_cast_le
deleted theorem Ordinal.nat_cast_lt
deleted theorem Ordinal.nat_cast_mod
deleted theorem Ordinal.nat_cast_mul
deleted theorem Ordinal.nat_cast_ne_zero
deleted theorem Ordinal.nat_cast_pos
deleted theorem Ordinal.nat_cast_sub
deleted theorem Ordinal.one_add_nat_cast
added theorem Ordinal.sup_natCast
deleted theorem Ordinal.sup_nat_cast
added theorem Ordinal.natCast_succ
deleted theorem Ordinal.nat_cast_succ
added theorem Ordinal.natCast_opow
deleted theorem Ordinal.nat_cast_opow
deleted theorem Linarith.nat_cast_nonneg