Commit 2025-03-13 23:54 c9d2c019

View on Github →

chore(Algebra/Group/Basic): rename mul_right_eq_self to mul_eq_left etc (#22587) See discussion of #22507, apparently mul_eq_left is used more often that mul_right_eq_self for the same kind of lemma.

Estimated changes

modified theorem div_eq_inv_self
modified theorem div_eq_self
added theorem left_eq_mul
added theorem left_ne_mul
added theorem mul_eq_left
added theorem mul_eq_right
deleted theorem mul_left_eq_self
deleted theorem mul_left_ne_self
added theorem mul_ne_left
added theorem mul_ne_right
deleted theorem mul_right_eq_self
deleted theorem mul_right_ne_self
added theorem right_eq_mul
added theorem right_ne_mul
deleted theorem self_eq_mul_left
deleted theorem self_eq_mul_right
deleted theorem self_ne_mul_left
deleted theorem self_ne_mul_right