mul_neg

Stream: Is there code for X?

[Scott Morrison]

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?

[Adam Topaz]

docs#mul_neg_eq_neg_mul_symm ?

[Scott Morrison]

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]

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]

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

[Adam Topaz]

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

[Thomas Browning]

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]

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