Zulip Chat Archive

Stream: Is there code for X?

Topic: mul_neg, neg_mul


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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