Zulip Chat Archive

Stream: new members

Topic: Reflexivity of equality


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

view this post on Zulip Johan Commelin (May 28 2020 at 12:10):

Use $$ maths $$

view this post on Zulip Johan Commelin (May 28 2020 at 12:11):

if h : a = b, then h.symm : b = a

view this post on Zulip Johan Commelin (May 28 2020 at 12:12):

Also rw [eq_comm] can be used to swap sides of an equality

view this post on Zulip Filippo A. E. Nuccio (May 28 2020 at 12:12):

Ah, ok; but can't cc do it on its own?

view this post on Zulip Johan Commelin (May 28 2020 at 12:12):

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

view this post on Zulip Filippo A. E. Nuccio (May 28 2020 at 12:12):

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

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

view this post on Zulip 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 RC\mathbb{R}\to\mathbb{C} is level 1, and 1\sqrt{-1} is now level 2. But I will stop (just) before all this x20x^2\geq0 stuff because it doesn't look sexy proving this stuff by hand.


Last updated: May 18 2021 at 16:25 UTC