# Zulip Chat Archive

## Stream: new members

### Topic: Reflexivity of equality

#### Filippo A. E. Nuccio (May 28 2020 at 12:09):

Playing with the complex number game (and having admittedly given a glance at Kevin Buzzard's solutions) I was trying to prove something to the effect that `(x y : $$\mathbb{R}$$) :x*x+y*y > 0`

. Kevin has proven that `(x y : R ) :x*x+y*y = 0 <-> x=0 and y=0`

so I was happily using that `(x y : R ) : x=0 and y=0 -> 0=x*x+y*y`

, but then Lean was not happy at all. It became happy again when I insisted that `(x y : R ) : x=0 and y=0 -> x*x+y*y = 0 `

and then I fell in despair as I realised that even `cc`

cannot convert `a=b `

into `b=a`

. Is this true, that there is no hope?

Side question: how to type in LaTeX in Zulip?

#### Johan Commelin (May 28 2020 at 12:10):

Use `$$ maths $$`

#### Johan Commelin (May 28 2020 at 12:11):

if `h : a = b`

, then `h.symm : b = a`

#### Johan Commelin (May 28 2020 at 12:12):

Also `rw [eq_comm]`

can be used to swap sides of an equality

#### Filippo A. E. Nuccio (May 28 2020 at 12:12):

Ah, ok; but can't `cc`

do it on its own?

#### Johan Commelin (May 28 2020 at 12:12):

I would expect that it does... but I don't use it that much.

#### Filippo A. E. Nuccio (May 28 2020 at 12:12):

hmm... good sign I should not use it either.

#### Johan Commelin (May 28 2020 at 12:18):

Anyway, to prove `x * x + y * y > 0`

you need lemmas like `add_pos`

and `sq_pos`

.

#### Kevin Buzzard (May 28 2020 at 14:08):

Today on Twitch I'll be running through some of the complex number game. I just completely re-ordered everything, so the map $\mathbb{R}\to\mathbb{C}$ is level 1, and $\sqrt{-1}$ is now level 2. But I will stop (just) before all this $x^2\geq0$ stuff because it doesn't look sexy proving this stuff by hand.

Last updated: May 18 2021 at 16:25 UTC