9 search results for "tag:"category:Mathematics/Arithmetic and Number Theory/Number theory""

Showing 1 - 9
  1. coq-bertrand

    No documentation

    Correctness of Knuth's algorithm for prime numbers
    category:Mathematics/Arithmetic and Number Theory/Number theory category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs based on external tools category:Miscellaneous/Extracted Programs/Arithmetic keyword:Knuth's algorithm keyword:prime numbers keyword:Bertrand's postulate logpath:Bertrand date:2020-10-10
    Laurent Théry
    8.12.0
    LGPL-2.1-or-later
    Used by 0 other packages
    11 Oct 2020
  2. coq-bignums

    No documentation

    Compatibility wrapper for rocq-bignums
    category:Miscellaneous/Coq Extensions category:Mathematics/Arithmetic and Number Theory/Number theory category:Mathematics/Arithmetic and Number Theory/Rational numbers keyword:integer numbers keyword:rational numbers keyword:arithmetic keyword:arbitrary-precision logpath:Bignums
    Laurent Théry Benjamin Grégoire Arnaud Spiwack Evgeny Makarov Pierre Letouzey
    9.0.0+rocq9.1
    LGPL-2.1-only
    Used by 10 other packages
    16 Sep 2025
  3. coq-gaia-numbers

    No documentation

    Implementation of the sets of numbers Z, Q, and R following Bourbaki's Elements of Mathematics in Coq
    category:Mathematics/Arithmetic and Number Theory/Number theory keyword:integers keyword:rational numbers keyword:real numbers logpath:gaia.numbers date:2024-07-24
    José Grimm Alban Quadrat
    2.2
    MIT
    Used by 0 other packages
    11 Aug 2024
  4. coq-gaia-ordinals

    No documentation

    Implementation and properties of ordinals in Coq using Mathematical Components
    category:Mathematics/Logic/Set theory category:Mathematics/Arithmetic and Number Theory/Number theory keyword:ordered sets keyword:ordinal arithmetic keyword:ordinal numbers keyword:cardinal numbers logpath:gaia.ordinals date:2024-07-24
    José Grimm Alban Quadrat
    2.2
    MIT
    Used by 1 other packages
    11 Aug 2024
  5. coq-gaia-schutte

    No documentation

    Implementation of ordinals in Coq following Schütte and Ackermann
    category:Mathematics/Arithmetic and Number Theory/Number theory keyword:ordinal arithmetic keyword:ordinal numbers logpath:gaia.schutte date:2024-07-24
    José Grimm Alban Quadrat
    2.2
    MIT
    Used by 1 other packages
    11 Aug 2024
  6. coq-gaia-stern

    No documentation

    Properties of Fibonacci numbers and the Stern diatomic sequence in Coq
    category:Mathematics/Arithmetic and Number Theory/Number theory keyword:Stern-Brocot keyword:fibonacci numbers logpath:gaia.stern date:2024-07-24
    José Grimm Alban Quadrat
    2.2
    MIT
    Used by 0 other packages
    11 Aug 2024
  7. coq-mathcomp-apery

    No documentation

    A formally verified proof in Coq, by computer algebra, that ζ(3) is irrational
    category:Mathematics/Arithmetic and Number Theory/Number theory keyword:apery recurrence keyword:irrationality keyword:creative telescoping logpath:mathcomp.apery date:2022-05-05
    Frédéric Chyzak Assia Mahboubi Thomas Sibut-Pinote
    1.0.2
    CECILL-C
    Used by 0 other packages
    05 May 2022
  8. coq-pocklington

    No documentation

    Pocklington's criterion in Coq
    category:Mathematics/Arithmetic and Number Theory/Number theory keyword:Pocklington keyword:number theory keyword:prime numbers keyword:primality keyword:Fermat's little theorem logpath:Pocklington date:2021-01-01
    Olga Caprotti Martijn Oostdijk
    8.12.0
    LGPL-2.1-or-later
    Used by 1 other packages
    02 Jan 2021
  9. rocq-bignums

    No documentation

    Bignums, the Rocq library of arbitrarily large numbers
    category:Miscellaneous/Coq Extensions category:Mathematics/Arithmetic and Number Theory/Number theory category:Mathematics/Arithmetic and Number Theory/Rational numbers keyword:integer numbers keyword:rational numbers keyword:arithmetic keyword:arbitrary-precision logpath:Bignums
    Laurent Théry Benjamin Grégoire Arnaud Spiwack Evgeny Makarov Pierre Letouzey
    9.0.0+rocq9.1
    LGPL-2.1-only
    Used by 1 other packages
    16 Sep 2025