Zulip Chat Archive

Stream: new members

Topic: How to define angle? Is function arccos available ?


view this post on Zulip Nga Ngo (May 03 2019 at 05:15):

Hi every one,
I am trying to formalize Sum of angles in a triangle Theorem. I need to define the angle ABC, where A=(a1,a2), B=(b1,b2) and C=(c1,c2) in \R^2. I have defined the distance between A and B, scale product of two vector. And now I am going to define angle by using arccos function. But I have not found out arccos function in Mathlib. Is it available here?
Thanks all!

view this post on Zulip Mario Carneiro (May 03 2019 at 05:23):

I was going to say it's a bit of work to roll your own, but I see that the imperial undergrads have beaten me to the punch. The arccos function is defined in analysis.complex.exponential.

view this post on Zulip Mario Carneiro (May 03 2019 at 05:28):

Better yet, the arg function will give you a number between negative pi and pi

view this post on Zulip Mario Carneiro (May 03 2019 at 05:30):

on second thought maybe that's not easier (and/or signed angles are not what you want)

view this post on Zulip Nga Ngo (May 03 2019 at 09:43):

Thanks Mario, I have found it by your way. Here is the way I define angle. Is it ok? Could you check it?

noncomputable def Distance (a b: array 2  ):  :=
sqrt ((a.read 1-b.read 1)^2 + (a.read 2-b.read 2)^2)
noncomputable def Angle (a b c: array 2 ) :  :=
arccos (((a.read 1-b.read 1)*(c.read 1-b.read 1)+
(a.read 2-b.read 2)*(c.read 2-b.read 2))/((Distance a b)*(Distance c b)))

view this post on Zulip Johan Commelin (May 03 2019 at 09:45):

@Nga Ngo If you paste your code between

```lean
code goes here
```

it will be formatted with syntax highlighting. (Note: you can edit your old post, if you want.)

view this post on Zulip Chris Hughes (May 03 2019 at 10:00):

I think the type of angles has been defined as a quotient group of R. Could be useful.

view this post on Zulip Nga Ngo (May 03 2019 at 15:14):

Nga Ngo If you paste your code between

```lean
code goes here
```

it will be formatted with syntax highlighting. (Note: you can edit your old post, if you want.)

Thanks @Johan Commelin , I did it.

view this post on Zulip Nga Ngo (May 03 2019 at 15:15):

I think the type of angles has been defined as a quotient group of R. Could be useful.

I don't understand what you said. Could you explain more detail. Thanks.

view this post on Zulip Patrick Massot (May 03 2019 at 15:17):

Hint: go to https://github.com/leanprover-community/mathlib On the top left corner, there is a search form. Enter "angle" and hit Enter

view this post on Zulip Nga Ngo (May 03 2019 at 15:30):

@Patrick Massot , Thank you so much. It's amazing!


Last updated: May 10 2021 at 19:16 UTC