Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-24 12:36 474f96ac

View on Github →

feat(geometry/euclidean/oriented_angle): more on relation to unoriented angles (#16215) Add more lemmas about the relation of oriented and unoriented angles; in particular, some involving real.angle.to_real and real.angle.sign.

Estimated changes

Modified src/geometry/euclidean/oriented_angle.lean

added theorem orientation.angle_eq_abs_oangle_to_real

added theorem orientation.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero

added theorem orientation.oangle_eq_iff_angle_eq_of_sign_eq

added theorem orientation.oangle_eq_of_angle_eq_of_sign_eq

added theorem orientation.oangle_eq_pi_iff_angle_eq_pi

added theorem orientation.oangle_eq_zero_iff_angle_eq_zero

added theorem orthonormal.angle_eq_abs_oangle_to_real

added theorem orthonormal.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero

added theorem orthonormal.oangle_eq_iff_angle_eq_of_sign_eq

added theorem orthonormal.oangle_eq_of_angle_eq_of_sign_eq

added theorem orthonormal.oangle_eq_pi_iff_angle_eq_pi

added theorem orthonormal.oangle_eq_zero_iff_angle_eq_zero