Zulip Chat Archive

Stream: new members

Topic: Confusion about add_eq_zero_iff


view this post on Zulip Patrick Lutz (Jun 05 2020 at 00:31):

When I try the following:

import data.real.basic

example (x y : ) : x*x + y*y = 0  x = 0  y = 0 :=
begin
    intro h,
    rw add_eq_zero_iff at h,
end

Lean tells me rewrite tactic failed, did not find instance of the pattern in the target expression _ = 0
Why is that? To me h obviously looks like an instance of add_eq_zero_iff. Is it because R\mathbb{R} is not a canonically_ordered_add_monoid which add_eq_zero_iff requires?

view this post on Zulip Kyle Miller (Jun 05 2020 at 00:45):

It doesn't seem like R\mathbb{R} should satisfy that. The monoid of non-negative reals under addition would, though, I think.

view this post on Zulip Patrick Lutz (Jun 05 2020 at 00:46):

Lol, oh yeah I somehow just realized I'm being stupid

view this post on Zulip Patrick Lutz (Jun 05 2020 at 00:47):

I didn't really think about what that theorem means

view this post on Zulip Patrick Lutz (Jun 05 2020 at 00:47):

It looks like what I really want is add_eq_zero_iff'

view this post on Zulip Alex J. Best (Jun 05 2020 at 00:48):

Or add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg

view this post on Zulip Alex J. Best (Jun 05 2020 at 00:50):

Which looks to be exactly the same lemma as add_eq_zero_iff_eq_zero_of_nonneg just with a longer name :rolling_on_the_floor_laughing:

view this post on Zulip Alex J. Best (Jun 05 2020 at 01:00):

So we should remove the two I just mentioned perhaps as they assume ordered_cancel_add_comm_monoid rather than ordered_add_comm_monoid

view this post on Zulip Kyle Miller (Jun 05 2020 at 01:00):

If you do library_search, it suggests exact mul_self_add_mul_self_eq_zero.mp which is exactly the theorem.

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 06:18):

Oh yeah, I still remember the day that I understood that "canonically ordered" means "a<=b iff there exists c such that b=a+c". So basically if you're canonical then everything is >=0. So basically it's just nat

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 06:18):

Computer scientists are so fixated with nat, it's crazy

view this post on Zulip Johan Commelin (Jun 05 2020 at 06:31):

What about nnreal?

view this post on Zulip Mario Carneiro (Jun 05 2020 at 06:52):

I think the general practice comes from monoid orders

view this post on Zulip Mario Carneiro (Jun 05 2020 at 06:53):

Any (add_)monoid can be canonically ordered

view this post on Zulip Kenny Lau (Jun 05 2020 at 06:55):

how do you canonically order Z\Bbb Z?

view this post on Zulip Mario Carneiro (Jun 05 2020 at 06:56):

I suppose the order is usually not a partial order though

view this post on Zulip Mario Carneiro (Jun 05 2020 at 06:56):

nat can be canonically ordered as a multiplicative monoid by divisibility

view this post on Zulip Mario Carneiro (Jun 05 2020 at 06:57):

int can be canonically ordered but the order is trivial

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 07:28):

Kenny you can canonically order any group, because any set is a category

view this post on Zulip Jalex Stark (Jun 05 2020 at 15:46):

do the nonnegative elements of an arbitrary ordered ring form a canonically ordered monoid?
(my motivating example is the cone of psd matrices, where you put an order on matrices AB A \le B if AB A - B is positive semi-definite)

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 22:33):

Wouldn't surprise me at all


Last updated: May 18 2021 at 17:44 UTC