mul_neg, neg_mul

Stream: Is there code for X?

[Eric Wieser]

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]

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]

First one is mul_neg_eq_neg_mul_symm... Yeah, those

[Eric Wieser]

#11925