Zulip Chat Archive

Stream: Is there code for X?

Topic: mul_neg


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

view this post on Zulip Adam Topaz (Mar 19 2021 at 01:29):

docs#mul_neg_eq_neg_mul_symm ?

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

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

view this post on Zulip Scott Morrison (Mar 19 2021 at 01:36):

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

view this post on Zulip Adam Topaz (Mar 19 2021 at 01:37):

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

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

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