Commit 2024-04-03 11:58 392a24a9

View on Github →

chore(Data/Int): Rename coe_nat to natCast (#11637) Reduce the diff of #11499

Renames

All in the Int namespace:

  • ofNat_eq_cast → ofNat_eq_natCast
  • cast_eq_cast_iff_Nat → natCast_inj
  • natCast_eq_ofNat → ofNat_eq_natCast
  • coe_nat_sub → natCast_sub
  • coe_nat_nonneg → natCast_nonneg
  • sign_coe_add_one → sign_natCast_add_one
  • nat_succ_eq_int_succ → natCast_succ
  • succ_neg_nat_succ → succ_neg_natCast_succ
  • coe_pred_of_pos → natCast_pred_of_pos
  • coe_nat_div → natCast_div
  • coe_nat_ediv → natCast_ediv
  • sign_coe_nat_of_nonzero → sign_natCast_of_ne_zero
  • toNat_coe_nat → toNat_natCast
  • toNat_coe_nat_add_one → toNat_natCast_add_one
  • coe_nat_dvd → natCast_dvd_natCast
  • coe_nat_dvd_left → natCast_dvd
  • coe_nat_dvd_right → dvd_natCast
  • le_coe_nat_sub → le_natCast_sub
  • succ_coe_nat_pos → succ_natCast_pos
  • coe_nat_modEq_iff → natCast_modEq_iff
  • coe_natAbs → natCast_natAbs
  • coe_nat_eq_zero → natCast_eq_zero
  • coe_nat_ne_zero → natCast_ne_zero
  • coe_nat_ne_zero_iff_pos → natCast_ne_zero_iff_pos
  • abs_coe_nat → abs_natCast
  • coe_nat_nonpos_iff → natCast_nonpos_iff Also rename Nat.coe_nat_dvd to Nat.cast_dvd_cast

Estimated changes

deleted theorem NNReal.coe_natAbs
added theorem NNReal.natCast_natAbs
deleted theorem Int.cast_eq_cast_iff_Nat
deleted theorem Int.coe_nat_div
deleted theorem Int.coe_nat_ediv
deleted theorem Int.coe_nat_inj'
deleted theorem Int.coe_nat_mod
deleted theorem Int.coe_nat_nonneg
deleted theorem Int.coe_pred_of_pos
added theorem Int.natCast_div
added theorem Int.natCast_ediv
added theorem Int.natCast_inj
added theorem Int.natCast_mod
added theorem Int.natCast_nonneg
added theorem Int.natCast_succ
deleted theorem Int.nat_succ_eq_int_succ
deleted theorem Int.ofNat_eq_cast
added theorem Int.ofNat_eq_natCast
deleted theorem Int.sign_coe_add_one
deleted theorem Int.succ_neg_nat_succ
deleted theorem Int.toNat_coe_nat
deleted theorem Int.toNat_coe_nat_add_one
added theorem Int.toNat_natCast
deleted theorem Int.coe_nat_dvd
deleted theorem Int.coe_nat_dvd_left
deleted theorem Int.coe_nat_dvd_right
added theorem Int.dvd_natCast
added theorem Int.natCast_dvd
deleted theorem Int.le_coe_nat_sub
added theorem Int.le_natCast_sub
deleted theorem Int.succ_coe_nat_pos
added theorem Int.succ_natCast_pos
deleted theorem Int.coe_nat_modEq_iff
added theorem Int.natCast_modEq_iff
deleted theorem Int.abs_coe_nat
added theorem Int.abs_natCast
deleted theorem Int.coe_natAbs
deleted theorem Int.coe_nat_eq_zero
deleted theorem Int.coe_nat_ne_zero
deleted theorem Int.coe_nat_nonpos_iff
added theorem Int.natCast_eq_zero
added theorem Int.natCast_natAbs
added theorem Int.natCast_ne_zero
added theorem Int.natCast_nonpos_iff
added theorem Nat.cast_dvd_cast
deleted theorem Nat.coe_nat_dvd