How to define angle? Is function arccos available ?

Stream: new members

[Nga Ngo]

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]

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]

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

[Mario Carneiro]

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

[Nga Ngo]

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]

@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]

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

[Nga Ngo]

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]

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]

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]

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