Zulip Chat Archive

Stream: general

Topic: triangles

Simon Hudon (Jun 29 2020 at 12:27):

With the current state of mathlib, how would one prove that the sum of the angles of a triangle is pi? So far, I've been using scalar product to define the angle between two segments but I'm not sure where to go from here.

Rob Lewis (Jun 29 2020 at 12:31):

https://github.com/leanprover-community/mathlib/blob/ca44926/src/geometry/euclidean.lean#L636

Johan Commelin (Jun 29 2020 at 12:35):

mathlib — grows faster than you think

Simon Hudon (Jun 29 2020 at 12:36):

Yeah, every time I blink ...

Simon Hudon (Jun 29 2020 at 12:36):

All that's missing is some CS

Johan Commelin (Jun 29 2020 at 12:36):

What do you mean :wink:

Last updated: Dec 20 2023 at 11:08 UTC