Commit 2022-10-12 10:35 b30449d6

View on Github →

feat(geometry/euclidean/oriented_angle): signs of angles and same_ray (#16909) Add more lemmas about signs of angles in relation to the order of points on a line.

Estimated changes

Modified src/geometry/euclidean/oriented_angle.lean

added theorem collinear.oangle_sign_of_same_ray_vsub

added theorem sbtw.oangle_sign_eq

added theorem sbtw.oangle_sign_eq_left

added theorem sbtw.oangle_sign_eq_right

added theorem wbtw.oangle_sign_eq_of_ne_left

added theorem wbtw.oangle_sign_eq_of_ne_right