square root

Stream: new members

[Shadman Sakib]

Is there a way to take the square root of a variable?

[Kevin Buzzard]

There is docs#real.sqrt and I guess you can raise a complex number to the power 1/2.

[Shadman Sakib]

Yes but how do I use it in lean. I want to take the square root of x^2

[Kevin Buzzard]

it's a function. Just apply it. Do you have a #mwe?

[Shadman Sakib]

idk what that is

[Kevin Buzzard]

click on it

[Shadman Sakib]

apply real.sqrt?

[Kevin Buzzard]

I cannot help unless you tell me far more precisely what you are talking about. Click on the link. Post some fully working code.

[Shadman Sakib]

oh

[Shadman Sakib]

okay

[Shadman Sakib]

example (x y : ℝ) : x^2 = y^2 → x = y ∨ x = -y :=
begin
intro hyp,

end

[Kevin Buzzard]

So it seems to me that you do not mean "how do I take the square root of x^2", you mean "how do I prove that the only square roots of x^2 are +-x".

[Shadman Sakib]

oh I was going to sqrt the x^2 to prove that lol

[Kevin Buzzard]

So you need to work on your #mwe skills and why not learn now. You post code between triple back ticks ``` , and "fully working" means that you have to include all imports etc, so that I can just cut and paste it to my VS Code and it will work.

[Kevin Buzzard]

If you sqrt the x^2 then you'll get sqrt(x^2).

[Shadman Sakib]

yeah and then sqrt(y^2) which will show x=y but i don't think you can do that right

[Kevin Buzzard]

You can just edit your post above -- try and make it into an #mwe. If you're going to ask a bunch of questions on on this site then it's really important that you quickly learn how to ask good questions.

[Kevin Buzzard]

Right now you seem to be confused between the sqrt function, and theorems about the sqrt function.

[Kevin Buzzard]

But when you've fixed up your mwe we can talk about this.

[Shadman Sakib]

import algebra.group.pi

set_option pp.beta true

example (x y : ℝ) : x^2 = y^2 → x = y ∨ x = -y :=
begin
 intro hyp,

end```

[Kevin Buzzard]

Use triple back ticks ``` on lines by themselves before and after your code. You can just edit your last post.

[Kevin Buzzard]

This information is included in the link.

[Kevin Buzzard]

You just need one ``` before the start of your code, and one ``` after the end of it.

[Shadman Sakib]

haha sorry, thanks for your patience

[Kevin Buzzard]

It's Ok. I see you're asking a bnuch of questions and this #mwe thing is something which works really well for communication on Zulip.

[Kevin Buzzard]

The answer to your question is that this looks like it is a standard fact about square roots, and so probably it is a theorem which is already in the library. So you can try library_search on the line after intro hyp, and see if you're lucky.

[Shadman Sakib]

yeah i can tell

[Kevin Buzzard]

and on this occasion it looks like you are lucky. You can click on the blue code where it says "Try this" and it will replace library_search with some code which works. You can then hover over the new code which has appeared and learn about it.

[Shadman Sakib]

ahhh it worked

[Kevin Buzzard]

The naming conventions #naming explain why the theorem is called that.

[Shadman Sakib]

ok, some commands are different they do not stand alone. why is that so?

[Shadman Sakib]

such as

[Kevin Buzzard]

After a while you can start guessing the names of theorems by yourself. I keep meaning to put a little quiz up for this sort of thing.

[Shadman Sakib]

dvd_refl

[Kevin Buzzard]

Do you understand the difference between tactic mode and term mode?

[Shadman Sakib]

import data.real.basic
example (a b : ℕ) : a ∣ b ↔ gcd a b = a :=
begin
  split,
  intro hyp,
  have my_hyp := dvd_refl a,
  apply nat.gcd_eq_left_iff_dvd,
end

[Kevin Buzzard]

dvd_refl is a term. library_search is a tactic. To learn about term mode I would recommend that you read the first few chapters of #tpil and do the exercises. To learn about tactic mode you can play the natural number game. Lean has a very high learning curve and both of these are designed to be beginner-friendly.

[Shadman Sakib]

Okay

[Shadman Sakib]

Thanks

[Kevin Buzzard]

Those last ``` s at the end should be on a line by themselves, not on the same line as the end

[Shadman Sakib]

okay

[Shadman Sakib]

i want to use the fact that a|a and a|b to just say gcd a b is a

[Shadman Sakib]

but im not sure how

[Kevin Buzzard]

Do you see the "copy code" link at the top right of your code block? Once you have it exactly right, people can just click there and instantly get your code onto their computer. This is why it's so important to get it right -- it makes other people's lives easier.

[Shadman Sakib]

Yeah, i fixed it i think it should be good now

[Shadman Sakib]

how would i finish up the proof? do you have any ideas?

[Eric Wieser]

The opening ``` need to be on a line by themselves too

[Eric Wieser]

If you fix that, zulip will syntax highlight your code. Right now it's throwing away your import line because it's on the same line

[Eric Wieser]

Can you fix your two posts above for practice? Thanks!

[Shadman Sakib]

Sorry

[Heather Macbeth]

It looks like the statement of the lemma nat.gcd_eq_left_iff_dvd is precisely the fact that you are trying to prove, namely

a ∣ b ↔ gcd a b = a

You can see this by looking at the lemma statement in the mathlib documentation -- click on the following link: docs#nat.gcd_eq_left_iff_dvd

[Heather Macbeth]

This means that you can prove the exercise just in the following way:

import data.real.basic
open nat

example (a b : ℕ) : a ∣ b ↔ gcd a b = a :=
begin
  exact nat.gcd_eq_left_iff_dvd,
end

[Shadman Sakib]

Ahh yeah, I used this term from that site. Just didn't know how to implement it. Thank you!

[Heather Macbeth]

However, since this exercise comes from the tutorials, I would guess that this is not how you are "supposed to" do it -- instead, there is probably a way of doing the exercise from first principles, using whatever lemmas are proved right before this in the tutorial.