diff options
| author | Avi Shinnar | 2020-12-05 21:56:15 -0500 |
|---|---|---|
| committer | Avi Shinnar | 2020-12-09 08:40:11 -0500 |
| commit | 29d2ffb5f5569efe8614efa30be560efc72a34f5 (patch) | |
| tree | 64d49df94da5c5b2d4d5674d7caacf7b36c29822 /doc | |
| parent | 9e0ca704fa8273a8337ff9e118d2d08620af8962 (diff) | |
Redefines exp_ineq1 to hold for all non-zero numbers.
The original (which holds only for positive numbers) is now called exp_ineq1_pos.
A version that holds only for negative numbers is added as exp_ineq1_neg.
Adds exp_ineq1_le, which holds for all reals (but is a <= instead of a <).
Co-authored-by: Barry M. Trager <bmt@us.ibm.com>
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/10-standard-library/13582-exp_ineq.rst | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/doc/changelog/10-standard-library/13582-exp_ineq.rst b/doc/changelog/10-standard-library/13582-exp_ineq.rst new file mode 100644 index 0000000000..27d89b2f8b --- /dev/null +++ b/doc/changelog/10-standard-library/13582-exp_ineq.rst @@ -0,0 +1,9 @@ +- **Changed:** + Minor Changes to Rpower: + Generalizes exp_ineq1 to hold for all non-zero numbers. + Adds exp_ineq1_le, which holds for all reals (but is a <= instead of a <). + + (`#13582 <https://github.com/coq/coq/pull/13582>`_, + by Avi Shinnar and Barry Trager, with help from Laurent Théry + +). |