## Stream: new members

#### 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,
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 $\mathbb{R}$ is not a canonically_ordered_add_monoid which add_eq_zero_iff requires?

#### Kyle Miller (Jun 05 2020 at 00:45):

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

#### Patrick Lutz (Jun 05 2020 at 00:46):

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

#### Patrick Lutz (Jun 05 2020 at 00:47):

I didn't really think about what that theorem means

#### Patrick Lutz (Jun 05 2020 at 00:47):

It looks like what I really want is add_eq_zero_iff'

#### Alex J. Best (Jun 05 2020 at 00:48):

Or add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg

#### 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:

#### 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

#### 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.

#### 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

#### Kevin Buzzard (Jun 05 2020 at 06:18):

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

#### Johan Commelin (Jun 05 2020 at 06:31):

What about nnreal?

#### Mario Carneiro (Jun 05 2020 at 06:52):

I think the general practice comes from monoid orders

#### Mario Carneiro (Jun 05 2020 at 06:53):

Any (add_)monoid can be canonically ordered

#### Kenny Lau (Jun 05 2020 at 06:55):

how do you canonically order $\Bbb Z$?

#### Mario Carneiro (Jun 05 2020 at 06:56):

I suppose the order is usually not a partial order though

#### Mario Carneiro (Jun 05 2020 at 06:56):

nat can be canonically ordered as a multiplicative monoid by divisibility

#### Mario Carneiro (Jun 05 2020 at 06:57):

int can be canonically ordered but the order is trivial

#### Kevin Buzzard (Jun 05 2020 at 07:28):

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

#### 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 $A \le B$ if $A - B$ is positive semi-definite)

#### Kevin Buzzard (Jun 05 2020 at 22:33):

Wouldn't surprise me at all

Last updated: May 18 2021 at 17:44 UTC