## Stream: Is there code for X?

### Topic: mul_neg

#### Scott Morrison (Mar 19 2021 at 01:27):

We surely can't be missing

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


What is it called?

#### Scott Morrison (Mar 19 2021 at 01:35):

Interesting. I wonder why I couldn't get either simp or library_search to find it. Looks like it must have been user error.

#### Scott Morrison (Mar 19 2021 at 01:36):

I think I was just an idiot and didn't try simp. Unfortunately library_search provides: exact norm_num.mul_pos_neg a b (a * b) rfl.

#### Scott Morrison (Mar 19 2021 at 01:36):

Perhaps I should forbid library_search from providing lemmas from norm_num..

#### Adam Topaz (Mar 19 2021 at 01:37):

That's not a very intuitive name anyway... Why the symm?

#### Thomas Browning (Mar 19 2021 at 01:40):

Scott Morrison said:

Perhaps I should forbid library_search from providing lemmas from norm_num..

and linarith too? (I often have linarith lemmas showing up in library search, and I would always rather have the non-linarith version)

#### Kevin Buzzard (Mar 19 2021 at 06:57):

I think that in general you don't know whether to push all negs outside or inside, and the moment you start using things with simp you're making the decision to go one way. My vague memory of norm_num is that it makes a concrete decision on this and tags a bunch of lemmas as simp lemmas locally

Last updated: May 07 2021 at 21:10 UTC