Triangle inequality for angles (PR, currently kinda wip)

Stream: mathlib4

[Ilmārs Cīrulis]

I'm currently working on suggestions of jsm28 in the #26129 and I hope it's okay to start discussion (or ask for help etc.) here.

Okay, I will start with some newbie questions:
1) How would you call the file which contains proof of triangle law for angles, but only for unit vectors? I have currently named it "UnitSphereAngles" (which is better than "TemporaryName", but not good on its own).
2) I made definition noncomputable def normalized (x : V) : V := ‖x‖⁻¹ • x. What do you think about its name? (Previously I had it named unit which was understandably rejected.)
3) Only first three theorems of Normalized.lean file are used in the proof (normalized_zero_eq_zero, norm_normalized_eq_one_iff, normalized_eq_self_of_norm_eq_one), but I probably should add some more results to this file. Maybe you have some suggestions in addition to the existing 5 theorems?

When all these questions are solved (or maybe even right now) I should work on documentation in these files.

[Ilmārs Cīrulis]

P.S. Big thanks to Alex Meiburg who helped so much!

[Ilmārs Cīrulis]

Proof was taken from these lecture notes
Should I link to them in some file?

[Ilmārs Cīrulis]

If I use namespace, for example, UnitVectors (in that badly named UnitSphereAngles :grimacing:), do I need to put _of_norm_one at the end of theorem names? Or maybe can I skip it and shorten theorem names?

[Ilmārs Cīrulis]

Renamed it (the UnitSphereAngles) to UnitVectorAngles, which seems better choice to me.

[Kevin Buzzard]

Re the lecture notes: reference them in the module docstring. I don't know if we usually put "random pdf off the internet" into the official mathlib references.

[Ilmārs Cīrulis]

Yes! All checks are green, did all I could. Now waiting for comments of Joseph Myers in the PR.