trigonometric): ranges of `real.sin` and `real.cos` (#3998)

Commit

5 years ago

feat(analysis/special_functions/trigonometric): ranges of `real.sin` and `real.cos` (#3998) Co-authored-by: Anatole Dedecker <48656793+ADedecker@users.noreply.github.com>

References

#4925 - Make prime-avoidance branch build

Author

ADedecker

Parents

d4484a4e

mathlib3 d0a8cc4b - feat(analysis/special_functions/trigonometric): ranges of `real.sin` and `real.cos` (#3998)

mathlib3
d0a8cc4b - feat(analysis/special_functions/trigonometric): ranges of `real.sin` and `real.cos` (#3998)