# Zulip Chat Archive

## Stream: new members

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

#### 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!

#### 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`

.

#### Mario Carneiro (May 03 2019 at 05:28):

Better yet, the `arg`

function will give you a number between negative pi and pi

#### 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)

#### 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)))

#### 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.)

#### 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.

#### 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.

#### 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.

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

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