-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(geometry/euclidean/oriented_angle): relation to unoriented angles #15722
Conversation
Add some versions of the result that an oriented angle is plus or minus the unoriented angle between the same two vectors. There will be a lot more lemmas to add subsequently in this area (including, in particular, lemmas about when two angles have the same or different signs, that are needed to go from equality of unoriented angles to equality of oriented angles). This just provides the starting point for adding such results.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
One optional comment but otherwise looks great :-)
bors d+
✌️ jsm28 can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
#15722) Add some versions of the result that an oriented angle is plus or minus the unoriented angle between the same two vectors. There will be a lot more lemmas to add subsequently in this area (including, in particular, lemmas about when two angles have the same or different signs, that are needed to go from equality of unoriented angles to equality of oriented angles). This just provides the starting point for adding such results.
Pull request successfully merged into master. Build succeeded: |
#15722) Add some versions of the result that an oriented angle is plus or minus the unoriented angle between the same two vectors. There will be a lot more lemmas to add subsequently in this area (including, in particular, lemmas about when two angles have the same or different signs, that are needed to go from equality of unoriented angles to equality of oriented angles). This just provides the starting point for adding such results.
#15722) Add some versions of the result that an oriented angle is plus or minus the unoriented angle between the same two vectors. There will be a lot more lemmas to add subsequently in this area (including, in particular, lemmas about when two angles have the same or different signs, that are needed to go from equality of unoriented angles to equality of oriented angles). This just provides the starting point for adding such results.
Add some versions of the result that an oriented angle is plus or
minus the unoriented angle between the same two vectors.
There will be a lot more lemmas to add subsequently in this area
(including, in particular, lemmas about when two angles have the same
or different signs, that are needed to go from equality of unoriented
angles to equality of oriented angles). This just provides the
starting point for adding such results.