diff options
| author | thery | 2019-03-19 14:26:11 +0100 |
|---|---|---|
| committer | Michael Soegtrop | 2020-04-01 16:12:14 +0200 |
| commit | aa9926492feaf8326f379469a555f77393fcd306 (patch) | |
| tree | 7ff538220fd143efe78c04f80b65bc208d959df0 /doc | |
| parent | 828b79f744ffc1f292a77a80553906544c1c0cfb (diff) | |
- Addition to the Reals theory :
- minus: lemmas `Rminus_eq_0` and `Rmult_minus_distr_r`
- sin : sin_inj
- cos : cos_inj
- sqrt : lemmas `pow2_sqrt` and `inv_sqrt`
- atan : lemmas `tan_inj`, `atan_eq0`, `atan_tan` and `tan_atan`
- asin : definition and some basic properties
- acos : definition and some basic properties
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/10-standard-library/00000-title.rst | 1 | ||||
| -rw-r--r-- | doc/changelog/10-standard-library/09803-trigo.rst | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/doc/changelog/10-standard-library/00000-title.rst b/doc/changelog/10-standard-library/00000-title.rst index d517a0e709..a182366f03 100644 --- a/doc/changelog/10-standard-library/00000-title.rst +++ b/doc/changelog/10-standard-library/00000-title.rst @@ -1,3 +1,2 @@ **Standard library** - diff --git a/doc/changelog/10-standard-library/09803-trigo.rst b/doc/changelog/10-standard-library/09803-trigo.rst new file mode 100644 index 0000000000..10cb069a4c --- /dev/null +++ b/doc/changelog/10-standard-library/09803-trigo.rst @@ -0,0 +1,2 @@ + +- Addition to the Reals theory (`#09803 <https://github.com/coq/coq/pull/09803>`_ by Laurent Théry): |