13 search results for "author:"Assia Mahboubi""

Showing 1 - 13
  1. coq-approx-models

    No documentation

    Rigorous approximations with a posteriori verified operations
    category:Mathematics/Approximation Theory keyword:approximation theory keyword:Chebyshev polynomials keyword:certificate-based approximation logpath:ApproxModels date:2021-06-15
    Florent Bréhard Assia Mahboubi Damien Pous
    1.0
    CECILL-B
    Used by 0 other packages
    16 Jun 2021
  2. coq-mathcomp-abel

    No documentation

    Abel - Ruffini's theorem
    keyword:algebra keyword:Galois keyword:Abel Ruffini keyword:unsolvability of quintincs logpath:Abel date:2022-07-13
    Sophie Bernard Cyril Cohen Assia Mahboubi Pierre-Yves Strub
    1.2.1
    CECILL-B
    Used by 0 other packages
    24 Oct 2022
  3. coq-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.8.0
    CECILL-C
    Used by 7 other packages
    19 Dec 2024
  4. coq-mathcomp-analysis-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.8.0
    CECILL-C
    Used by 0 other packages
    19 Dec 2024
  5. 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
  6. coq-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.8.0
    CECILL-C
    Used by 2 other packages
    19 Dec 2024
  7. coq-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.8.0
    CECILL-C
    Used by 1 other packages
    19 Dec 2024
  8. coq-mathcomp-field-extra

    No documentation

    Extra Mathematical Components Library on Fields
    keyword:algebra keyword:field keyword:small scale reflection keyword:mathematical components keyword:odd order theorem
    Jeremy Avigad <> Andrea Asperti <> Stephane Le Roux <> Yves Bertot <> Laurence Rideau <> et al.
    1.6.1
    CeCILL-B
    Used by 1 other packages
    26 Jun 2019
  9. coq-mathcomp-odd-order

    No documentation

    The formal proof of the Feit-Thompson theorem
    keyword:finite groups keyword:Feit Thompson theorem keyword:small scale reflection keyword:mathematical components keyword:odd order theorem
    Jeremy Avigad <> Andrea Asperti <> Stephane Le Roux <> Yves Bertot <> Laurence Rideau <> et al.
    2.0.0
    CeCILL-B
    Used by 0 other packages
    18 Oct 2023
  10. coq-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.2
    CECILL-B
    Used by 5 other packages
    14 Dec 2024
  11. coq-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.8.0
    CECILL-C
    Used by 3 other packages
    19 Dec 2024
  12. coq-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.8.0
    CECILL-C
    Used by 2 other packages
    19 Dec 2024
  13. coq-ssreflect

    No documentation

    The Small Scale Reflection extension
    Jeremy Avigad <> Andrea Asperti <> Stephane Le Roux <> Yves Bertot <> Laurence Rideau <> et al.
    1.5.0
    CeCILL-B
    Used by 3 other packages
    13 May 2019