Commit 2022-10-11 03:45 34c70db6

View on Github →

feat(geometry/euclidean/oriented_angle): oriented angles and betweenness (#16824) Add lemmas relating oriented angles to strict and weak betweenness of points.

Estimated changes

Modified src/geometry/euclidean/oriented_angle.lean

added theorem collinear.two_zsmul_oangle_eq_left

added theorem collinear.two_zsmul_oangle_eq_right

added theorem euclidean_geometry.oangle_eq_pi_iff_sbtw

added theorem euclidean_geometry.oangle_eq_zero_iff_wbtw

added theorem sbtw.oangle_eq_add_pi_left

added theorem sbtw.oangle_eq_add_pi_right

added theorem sbtw.oangle_eq_left

added theorem sbtw.oangle_eq_left_right

added theorem sbtw.oangle_eq_right

added theorem sbtw.oangle₁₂₃_eq_pi

added theorem sbtw.oangle₁₃₂_eq_zero

added theorem sbtw.oangle₂₁₃_eq_zero

added theorem sbtw.oangle₂₃₁_eq_zero

added theorem sbtw.oangle₃₁₂_eq_zero

added theorem sbtw.oangle₃₂₁_eq_pi

added theorem wbtw.oangle_eq_left

added theorem wbtw.oangle_eq_right

added theorem wbtw.oangle₁₃₂_eq_zero

added theorem wbtw.oangle₂₁₃_eq_zero

added theorem wbtw.oangle₂₃₁_eq_zero

added theorem wbtw.oangle₃₁₂_eq_zero