Commit 2024-06-08 08:17 c1379a3c

View on Github →

chore(AddChar): Rename map_zero_one to map_zero_eq_one (#13576) To follow the naming convention, rename

  • map_zero_one → map_zero_eq_one
  • map_add_mul → map_add_eq_mul
  • map_nsmul_pow → map_nsmul_eq_pow
  • map_neg_inv → map_neg_eq_inv
  • map_zsmul_zpow → map_zsmul_eq_zpow

Estimated changes

modified theorem AddChar.inv_apply'
added theorem AddChar.map_add_eq_mul
deleted theorem AddChar.map_add_mul
added theorem AddChar.map_neg_eq_inv
deleted theorem AddChar.map_neg_inv
deleted theorem AddChar.map_nsmul_pow
deleted theorem AddChar.map_zero_one
deleted theorem AddChar.map_zsmul_zpow