27 search results for "tag:"logpath:mathcomp""

Showing 1 - 27
  1. coq-mathcomp-algebra-tactics

    No documentation

    Ring, field, lra, nra, and psatz tactics for Mathematical Components
    logpath:mathcomp.algebra_tactics
    Kazuhiko Sakaguchi Pierre Roux
    1.2.7
    CECILL-B
    Used by 4 other packages
    05 Sep 2025
  2. 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
  3. coq-mathcomp-bigenough

    No documentation

    Compatibility package for rocq-mathcomp-bigenough
    keyword:bigenough keyword:asymptotic reasonning keyword:small scale reflection keyword:mathematical components logpath:mathcomp.bigenough
    Cyril Cohen
    1.0.4
    CeCILL-B
    Used by 8 other packages
    23 Feb 2026
  4. coq-mathcomp-dioid

    No documentation

    Dioid
    keyword:dioid keyword:semiring keyword:complete dioid category:Miscellaneous/Coq Extensions logpath:mathcomp.dioid
    Lucien Rakotomalala <lucien.rakotomalala@onera.fr> Pierre Roux <pierre.roux@onera.fr>
    0.2
    CECILL-B
    Used by 0 other packages
    20 Dec 2021
  5. coq-mathcomp-finmap

    No documentation

    Compatibility package for rocq-mathcomp-finmap
    keyword:finmap keyword:finset keyword:multiset logpath:mathcomp.finmap
    Cyril Cohen Kazuhiko Sakaguchi
    2.2.4
    CECILL-B
    Used by 7 other packages
    24 Jul 2026
  6. coq-mathcomp-sum-of-two-square

    No documentation

    A proof of Fermat's theorem on sum of two squares. It is the proof that uses gaussian integers. This is done in ssreflect. It contains two file :
    logpath:mathcomp.contrib.sum_of_two_square
    Laurent Thery
    1.0.1
    MIT
    Used by 0 other packages
    09 May 2018
  7. coq-mathcomp-tarjan

    No documentation

    Strongly connected component algorithms by Tarjan and Kosaraju using Coq and MathComp
    category:Computer Science/Graph Theory keyword:strongly connected components keyword:topological sorting keyword:Kosaraju keyword:Tarjan keyword:acyclicity keyword:graph theory logpath:mathcomp.tarjan date:2023-08-06
    Cyril Cohen Jean-Jacques Lévy Karl Palmskog Laurent Théry
    1.0.5
    CECILL-B
    Used by 0 other packages
    24 Jul 2026
  8. coq-mathcomp-word

    No documentation

    Yet Another Coq Library on Machine Words
    category:Computer Science/Data Types and Data Structures keyword:machine words logpath:mathcomp.word date:2026-07-24
    Pierre-Yves Strub
    3.5
    MIT
    Used by 0 other packages
    24 Jul 2026
  9. rocq-mathcomp-algebra

    No documentation

    Mathematical Components Library on Algebra
    keyword:small scale reflection keyword:mathematical components keyword:algebra keyword:algebraic structure hierarchies keyword:archimedean field keyword:floor keyword:ceil keyword:intervals keyword:matrices keyword:vectors keyword:block matrices keyword:determinant keyword:Cramer rule keyword:Vandermonde matrices keyword:LUP decomposition keyword:Gaussian elimination keyword:matrix rank keyword:eigen values keyword:single variable polynomials keyword:bivariate polynomials keyword:polynomial division keyword:integers keyword:rational numbers keyword:semirings keyword:rings keyword:left algebra keyword:left module keyword:unit rings keyword:field keyword:algebraically closed field keyword:additive morphisms keyword:ring morphisms keyword:finite dimensional vector spaces keyword:complex numbers keyword:square root logpath:mathcomp.algebra
    The Mathematical Components team
    2.6.0
    CECILL-B
    Used by 13 other packages
    24 Jul 2026
  10. rocq-mathcomp-analysis

    No documentation

    An analysis library for mathematical components
    category:Mathematics/Real Calculus and Topology keyword:analysis keyword:Cantor keyword:topology keyword:real numbers keyword:sequence keyword:convexity keyword:Landau notation keyword:logarithm keyword:sin keyword:cos keyword:tangent keyword:trigonometric function keyword:exponential keyword:differentiation keyword:derivative keyword:measure theory keyword:integration keyword:Lebesgue keyword:probability logpath:mathcomp.analysis
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.18.0
    CECILL-C
    Used by 3 other packages
    07 Sep 2026
  11. rocq-mathcomp-analysis-stdlib

    No documentation

    A library to link real numbers from mathematical components and Stdlib
    category:Mathematics/Real Numbers category:Mathematics/Real Calculus and Topology keyword:real numbers keyword:reals logpath:mathcomp.reals_stdlib
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.18.0
    CECILL-C
    Used by 1 other packages
    07 Sep 2026
  12. rocq-mathcomp-bigenough

    No documentation

    A small library to do epsilon - N reasoning
    keyword:bigenough keyword:asymptotic reasonning keyword:small scale reflection keyword:mathematical components logpath:mathcomp.bigenough
    Cyril Cohen
    1.0.4
    CeCILL-B
    Used by 5 other packages
    23 Feb 2026
  13. rocq-mathcomp-boot

    No documentation

    Small Scale Reflection
    keyword:small scale reflection keyword:mathematical components keyword:bigop keyword:big operators keyword:biomial coefficient keyword:integer division theory keyword:finite sets keyword:functions with finite domain keyword:finite graphs keyword:quotient types keyword:lists keyword:ordering and sorting lists keyword:prime numbers keyword:tuples keyword:bounded lists logpath:mathcomp.boot
    The Mathematical Components team
    2.6.0
    CECILL-B
    Used by 5 other packages
    24 Jul 2026
  14. rocq-mathcomp-classical

    No documentation

    A library for classical logic for mathematical components
    category:Mathematics/Logic/Classical logic keyword:classical logic keyword:logic keyword:sets keyword:set theory keyword:function keyword:cardinal keyword:filter logpath:mathcomp.classical
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.18.0
    CECILL-C
    Used by 1 other packages
    07 Sep 2026
  15. rocq-mathcomp-experimental-reals

    No documentation

    A library for alternative real numbers for mathematical components
    category:Mathematics/Real Numbers keyword:real numbers keyword:reals logpath:mathcomp.experimental_reals
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.18.0
    CECILL-C
    Used by 0 other packages
    07 Sep 2026
  16. rocq-mathcomp-field

    No documentation

    Mathematical Components Library on Fields
    keyword:small scale reflection keyword:mathematical components keyword:algebra keyword:field logpath:mathcomp.field
    The Mathematical Components team
    2.6.0
    CECILL-B
    Used by 7 other packages
    24 Jul 2026
  17. rocq-mathcomp-finite-group

    No documentation

    Mathematical Components Library on finite groups
    keyword:small scale reflection keyword:mathematical components keyword:finite groups logpath:mathcomp.finite_group
    The Mathematical Components team
    2.6.0
    CECILL-B
    Used by 3 other packages
    24 Jul 2026
  18. rocq-mathcomp-finmap

    No documentation

    Finite sets, finite maps, finitely supported functions
    keyword:finmap keyword:finset keyword:multiset logpath:mathcomp.finmap
    Cyril Cohen Kazuhiko Sakaguchi
    2.2.4
    CECILL-B
    Used by 4 other packages
    24 Jul 2026
  19. rocq-mathcomp-group-representation

    No documentation

    Mathematical Components Library on group representation theory
    keyword:small scale reflection keyword:mathematical components keyword:algebra keyword:character keyword:group representation logpath:mathcomp.group_representation
    The Mathematical Components team
    2.6.0
    CECILL-B
    Used by 2 other packages
    24 Jul 2026
  20. rocq-mathcomp-hollight-real-with-N

    No documentation

    HOL-Light definition of real numbers in Rocq using N and MathComp
    logpath:MathComp_HOLLight_Real_With_N date:2025-07-11 category:Mathematics/Arithmetic and Number Theory/Miscellaneous category:Mathematics/Real Numbers keyword:HOL-Light
    https://github.com/Deducteam/mathcomp-hollight-real-with-N/blob/main/AUTHORS.md
    0.0.0
    CeCILL-2.1
    Used by 2 other packages
    02 Oct 2025
  21. rocq-mathcomp-multinomials

    No documentation

    A Multivariate polynomial Library for the Mathematical Components Library
    keyword:multinomials keyword:monoid algebra category:Mathematics/Algebra/Multinomials category:Mathematics/Algebra/Monoid algebra logpath:mathcomp.multinomials
    Pierre-Yves Strub
    2.5.0
    CECILL-B
    Used by 1 other packages
    24 Jul 2026
  22. rocq-mathcomp-order

    No documentation

    Mathematical Components Library on order theory
    keyword:small scale reflection keyword:mathematical components keyword:order theory keyword:partial order keyword:lattices keyword:total order logpath:mathcomp.order
    The Mathematical Components team
    2.6.0
    CECILL-B
    Used by 3 other packages
    24 Jul 2026
  23. rocq-mathcomp-real-closed

    No documentation

    Mathematical Components Library on real closed fields
    keyword:real closed field logpath:mathcomp.real_closed date:2024-12-09
    Cyril Cohen Assia Mahboubi
    2.0.6
    CECILL-B
    Used by 2 other packages
    24 Jul 2026
  24. rocq-mathcomp-reals

    No documentation

    A library for real numbers for mathematical components
    category:Mathematics/Real Numbers keyword:real numbers keyword:reals keyword:extended real numbers logpath:mathcomp.reals
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.18.0
    CECILL-C
    Used by 2 other packages
    07 Sep 2026
  25. rocq-mathcomp-reals-stdlib

    No documentation

    A library to link real numbers from mathematical components and Stdlib
    category:Mathematics/Real Numbers keyword:real numbers keyword:reals logpath:mathcomp.reals_stdlib
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.18.0
    CECILL-C
    Used by 1 other packages
    07 Sep 2026
  26. rocq-mathcomp-solvable

    No documentation

    Mathematical Components Library on finite groups (II)
    keyword:small scale reflection keyword:mathematical components keyword:finite groups logpath:mathcomp.solvable
    The Mathematical Components team
    2.6.0
    CECILL-B
    Used by 6 other packages
    24 Jul 2026
  27. rocq-mathcomp-zify

    No documentation

    Micromega tactics for Mathematical Components
    logpath:mathcomp.zify
    Kazuhiko Sakaguchi
    1.7.0+2.4+9.0
    CECILL-B
    Used by 2 other packages
    28 Aug 2026