Commit 2022-02-09 09:56 3aa5b8a9

refactor(algebra/ring/basic): rename lemmas about a*(-b) and (-a)*b (#11925) This renames:

• (- a) * b = - (a * b) from neg_mul_eq_neg_mul_symm to neg_mul
• a * (-b) = - (a * b) from mul_neg_eq_neg_mul_symm to mul_neg The new names are much easier to find when compared with sub_mul, mul_sub etc, and match the existing namespaced names under units and matrix. This also replaces rewrites by ← neg_mul_eq_neg_mul with neg_mul and rewrites by ← neg_mul_eq_mul_neg with mul_neg. To avoid clashes, the names in the matrix namespace are now protected. Zulip