blob: 86c5e45bc1e22b75bf1928d0f3216297c9b87f8f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
- **Changed:**
Cleanup of names in the Reals theory: replaced `tan_is_inj` with `tan_inj` and replaced `atan_right_inv` with `tan_atan` -
compatibility notations are provided. Moved various auxiliary lemmas from `Ratan.v` to more appropriate places.
(`#9803 <https://github.com/coq/coq/pull/9803>`_,
by Laurent Théry and Michael Soegtrop).
- **Added:** to the Reals theory:
inverse trigonometric functions `asin` and `acos` with lemmas for the derivatives, bounds and special values of these functions;
an extensive set of identities between trigonometric functions and their inverse functions;
lemmas for the injectivity of sine and cosine;
lemmas on the derivative of the inverse of decreasing functions and on the derivative of horizontally mirrored functions;
various generic auxiliary lemmas and definitions for Rsqr, sqrt, posreal an others.
(`#9803 <https://github.com/coq/coq/pull/9803>`_,
by Laurent Théry and Michael Soegtrop).
|
