mathlib
3aa5b8a9 - refactor(algebra/ring/basic): rename lemmas about `a*(-b)` and `(-a)*b` (#11925)

Commit
4 years ago
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](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/mul_neg.2C.20neg_mul/near/233638226)
Author
Parents
Loading