basic): angles and betweenness (#16734)

Commit

3 years ago

feat(geometry/euclidean/basic): angles and betweenness (#16734) Add some basic lemmas about the relation between (unoriented) angles and betweenness of points.

Author

jsm28

Parents

b0b0d5e3

mathlib3 6d5dda18 - feat(geometry/euclidean/basic): angles and betweenness (#16734)

mathlib3
6d5dda18 - feat(geometry/euclidean/basic): angles and betweenness (#16734)