# Zulip Chat Archive

## Stream: new members

### Topic: Confusion about add_eq_zero_iff

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