Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-24 21:27 f1f166b2

View on Github →

feat(geometry/euclidean/oriented_angle): angles equal to 0 or π (#16229) Add lemmas about various conditions for oriented angles between two vectors to equal 0 or π.

Estimated changes

Modified src/geometry/euclidean/oriented_angle.lean

added theorem orientation.oangle_eq_pi_iff_oangle_rev_eq_pi

added theorem orientation.oangle_eq_pi_iff_same_ray_neg

added theorem orientation.oangle_eq_zero_iff_oangle_rev_eq_zero

added theorem orientation.oangle_eq_zero_iff_same_ray

added theorem orientation.oangle_eq_zero_or_eq_pi_iff_not_linear_independent

added theorem orientation.oangle_eq_zero_or_eq_pi_iff_right_eq_smul

added theorem orientation.oangle_ne_zero_and_ne_pi_iff_linear_independent

added theorem orthonormal.oangle_eq_pi_iff_oangle_rev_eq_pi

added theorem orthonormal.oangle_eq_pi_iff_same_ray_neg

added theorem orthonormal.oangle_eq_zero_iff_oangle_rev_eq_zero

added theorem orthonormal.oangle_eq_zero_iff_same_ray

added theorem orthonormal.oangle_eq_zero_or_eq_pi_iff_not_linear_independent

added theorem orthonormal.oangle_eq_zero_or_eq_pi_iff_right_eq_smul

added theorem orthonormal.oangle_ne_zero_and_ne_pi_iff_linear_independent