angle): absolute value lemmas (#17485)

Commit

3 years ago

feat(analysis/special_functions/trigonometric/angle): absolute value lemmas (#17485) Add a series of lemmas involving absolute values of `sin`, `cos` and `to_real` of angles.

Author

jsm28

Parents

e9d89fee

mathlib3 f9c5995b - feat(analysis/special_functions/trigonometric/angle): absolute value lemmas (#17485)

mathlib3
f9c5995b - feat(analysis/special_functions/trigonometric/angle): absolute value lemmas (#17485)