Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-02 09:34 ddc74844

View on Github →

feat(geometry/euclidean/oriented_angle): signs of angles between linear combinations of vectors (#16243) Add a series of lemmas giving the sign of the oriented angle between two linear combinations of two vectors in terms of the sign of the angle between the original two vectors and the coefficients in the linear combination.

Estimated changes

Modified src/geometry/euclidean/oriented_angle.lean

added theorem orientation.oangle_sign_add_smul_left

added theorem orientation.oangle_sign_neg_left

added theorem orientation.oangle_sign_neg_right

added theorem orientation.oangle_sign_smul_add_right

added theorem orientation.oangle_sign_smul_add_smul_left

added theorem orientation.oangle_sign_smul_add_smul_right

added theorem orientation.oangle_sign_smul_add_smul_smul_add_smul

added theorem orientation.oangle_sign_smul_left

added theorem orientation.oangle_sign_smul_right

added theorem orientation.oangle_sign_sub_smul_left

added theorem orientation.oangle_sign_sub_smul_right

added theorem orthonormal.oangle_sign_add_smul_left

added theorem orthonormal.oangle_sign_neg_left

added theorem orthonormal.oangle_sign_neg_right

added theorem orthonormal.oangle_sign_smul_add_right

added theorem orthonormal.oangle_sign_smul_add_smul_left

added theorem orthonormal.oangle_sign_smul_add_smul_right

added theorem orthonormal.oangle_sign_smul_add_smul_smul_add_smul

added theorem orthonormal.oangle_sign_smul_left

added theorem orthonormal.oangle_sign_smul_right

added theorem orthonormal.oangle_sign_sub_smul_left

added theorem orthonormal.oangle_sign_sub_smul_right

added theorem orthonormal.oangle_smul_add_right_eq_zero_or_eq_pi_iff