Zulip Chat Archive

Stream: general

Topic: triangles


view this post on Zulip 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.

view this post on Zulip Rob Lewis (Jun 29 2020 at 12:31):

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

view this post on Zulip Johan Commelin (Jun 29 2020 at 12:35):

mathlib — grows faster than you think

view this post on Zulip Simon Hudon (Jun 29 2020 at 12:36):

Yeah, every time I blink ...

view this post on Zulip Simon Hudon (Jun 29 2020 at 12:36):

All that's missing is some CS

view this post on Zulip Johan Commelin (Jun 29 2020 at 12:36):

What do you mean :wink:


Last updated: May 09 2021 at 19:11 UTC