## Stream: Is there code for X?

### Topic: mul_neg, neg_mul

#### Eric Wieser (Apr 08 2021 at 11:42):

Do we really not have these?

lemma mul_neg {R : Type*} [ring R] (a b : R) : a * -b = -(a * b) := sorry
lemma neg_mul {R : Type*} [ring R] (a b : R) : (-a) * b = -(a * b) := sorry


#### Eric Wieser (Apr 08 2021 at 11:45):

Oh, they have the super long names docs#neg_mul_eq_neg_mul_symm and docs#mul_neg_eq_neg_mul_symm

#### Ruben Van de Velde (Apr 08 2021 at 11:45):

First one is mul_neg_eq_neg_mul_symm... Yeah, those

Last updated: May 17 2021 at 15:13 UTC