Commit 2022-07-27 17:03 63eb48be
View on Github →feat(analysis/special_functions/trigonometric/angle): equality of cos or sin (#15651)
analysis.special_functions.trigonometric.angle has results relating
equality of real.cos of two reals, or real.sin of two reals, to
relations between those reals converted to angle. Add variants of
those results where one or both of the arguments are passed as angle
instead of as reals, with real.angle.cos and real.angle.sin used
on those angle arguments.
The version for cos with one angle and one real argument, in
particular, is what I want for proving that the oriented angle between
two nonzero vectors is plus or minus the unoriented angle.