diff options
Diffstat (limited to 'doc/sphinx/addendum/nsatz.rst')
| -rw-r--r-- | doc/sphinx/addendum/nsatz.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst index ef9b3505d..387d61495 100644 --- a/doc/sphinx/addendum/nsatz.rst +++ b/doc/sphinx/addendum/nsatz.rst @@ -19,7 +19,7 @@ where :math:`P, Q, P₁,Q₁,\ldots,Pₛ, Qₛ` are polynomials and :math:`A` is domain, i.e. a commutative ring with no zero divisor. For example, :math:`A` can be :math:`\mathbb{R}`, :math:`\mathbb{Z}`, or :math:`\mathbb{Q}`. Note that the equality :math:`=` used in these goals can be -any setoid equality (see :ref:`TODO-27.2.2`) , not only Leibnitz equality. +any setoid equality (see :ref:`tactics-enabled-on-user-provided-relations`) , not only Leibnitz equality. It also proves formulas |