Commit 2024-08-12 15:04 f57201f9

View on Github →

chore: deduplicate inv_mul_cancel/mul_inv_cancel, etc. (#15717)

  • mul_left_inv, inv_mul_self → inv_mul_cancel (for Group)
  • mul_right_inv, mul_inv_self → mul_inv_cancel
  • add_left_neg, neg_add_self → neg_add_cancel (for AddGroup)
  • add_right_neg, add_neg_self → add_neg_cancel
  • inv_mul_cancel → inv_mul_cancel₀ (for GroupWithZero)
  • mul_inv_cancel → mul_inv_cancel₀

Estimated changes

modified theorem inv_smul_smul
modified theorem smul_inv_smul
modified theorem div_self'
added theorem inv_mul_cancel
deleted theorem inv_mul_self
added theorem mul_inv_cancel
deleted theorem mul_inv_self
deleted theorem mul_left_inv
deleted theorem mul_right_inv
modified theorem Group.isUnit
modified theorem div_self_mul_self
added theorem mul_inv_mul_cancel
deleted theorem mul_inv_mul_self
deleted theorem mul_inv_cancel
added theorem mul_inv_cancel₀
deleted theorem inv_mul_cancel
added theorem inv_mul_cancel₀