9 search results for "tag:"date:2025-12""

Showing 1 - 9
  1. coq-kruskal-fan

    No documentation

    Extending Coq library for manipulating Almost Full relations with the FAN theorem
    category:Computer Science/Data Types and Data Structures date:2025-12-11 logpath:KruskalFanProp logpath:KruskalFanType
    Dominique Larchey-Wendling (https://github.com/DmxLarchey)
    2.0
    MPL-2.0
    Used by 3 other packages
    08 Jan 2026
  2. coq-kruskal-higman

    No documentation

    Extending Coq library for manipulating Almost Full relations with Higman's lemma
    category:Computer Science/Data Types and Data Structures date:2025-12-11 logpath:KruskalHigmanProp logpath:KruskalHigmanType
    Dominique Larchey-Wendling (https://github.com/DmxLarchey)
    2.0
    MPL-2.0
    Used by 2 other packages
    08 Jan 2026
  3. coq-kruskal-theorems

    No documentation

    Extending the Coq library for manipulating Almost Full relations with various forms of Kruskal's tree theorem
    category:Computer Science/Data Types and Data Structures date:2025-12-11 logpath:KruskalThmProp logpath:KruskalThmType
    Dominique Larchey-Wendling (https://github.com/DmxLarchey)
    2.0
    MPL-2.0
    Used by 1 other packages
    08 Jan 2026
  4. coq-kruskal-veldman

    No documentation

    Wim Veldman's proof of Higman's and Kruskal tree theorems
    category:Computer Science/Data Types and Data Structures date:2025-12-11 logpath:KruskalVeldmanProp logpath:KruskalVeldmanType
    Dominique Larchey-Wendling (https://github.com/DmxLarchey)
    2.0
    MPL-2.0
    Used by 1 other packages
    08 Jan 2026
  5. rocq-num-analysis-algebra

    No documentation

    Algebraic structures for numerical analysis in Rocq
    category:Math/Algebra date:2025-12 logpath:NumAnalysis.Algebra keyword:algebra keyword:algebraic structure hierarchy keyword:functions to an algebraic structure keyword:algebraic substructure keyword:morphism keyword:monoid keyword:group keyword:ring keyword:module space keyword:affine space keyword:dimension theorem keyword:incomplete basis theorem keyword:dual basis keyword:predual basis keyword:rank-nullity theorem keyword:binomial coefficient
    Sylvie Boldo François Clément Vincent Martin Micaela Mayero Florian Faissole et al.
    2.1.0
    LGPL-3.0-or-later
    Used by 2 other packages
    27 Nov 2025
  6. rocq-num-analysis-fem

    No documentation

    The finite element method
    category:Math/Real Calculus and Topology date:2025-12 logpath:NumAnalysis.FEM keyword:multi-index keyword:multi-variate polynomial keyword:Lagrange polynomial keyword:finite element keyword:simplicial Lagrange finite element
    Sylvie Boldo François Clément Vincent Martin Micaela Mayero Florian Faissole et al.
    2.1.0
    LGPL-3.0-or-later
    Used by 1 other packages
    27 Nov 2025
  7. rocq-num-analysis-lax-milgram

    No documentation

    Lax-Milgram theorem
    category:Math/Real Calculus and Topology date:2025-12 logpath:NumAnalysis.LM keyword:fixed point theorem (in a Banach space) keyword:orthogonal projection keyword:orthogonal complement keyword:Riesz-Fréchet representation theorem keyword:Lax-Milgram theorem keyword:Céa's lemma
    Sylvie Boldo François Clément Vincent Martin Micaela Mayero Florian Faissole et al.
    2.1.0
    LGPL-3.0-or-later
    Used by 1 other packages
    27 Nov 2025
  8. rocq-num-analysis-lebesgue

    No documentation

    Lebesgue integral
    category:Math/Real Calculus and Topology date:2025-12 logpath:NumAnalysis.Lebesgue keyword:sigma-algebra keyword:monotone class theorem keyword:Dynkin pi-lambda theorem keyword:measure theory keyword:Lebesgue measure keyword:simple function keyword:adapted sequence keyword:Beppo Levi (monotone convergence) theorem keyword:Fatou lemma keyword:Lebesgue (dominated convergence) theorem keyword:Lebesgue induction principle keyword:Tonelli theorem keyword:Bochner integral
    Sylvie Boldo François Clément Vincent Martin Micaela Mayero Florian Faissole et al.
    2.1.0
    LGPL-3.0-or-later
    Used by 1 other packages
    27 Nov 2025
  9. rocq-num-analysis-subset

    No documentation

    Subsets for numerical analysis in Rocq
    category:Math/Logic/Set theory date:2025-12 logpath:NumAnalysis.Requisite logpath:NumAnalysis.Logic logpath:NumAnalysis.Numbers logpath:NumAnalysis.Subsets keyword:subset keyword:function keyword:homogeneous binary relation keyword:operation on finite families
    Sylvie Boldo François Clément Vincent Martin Micaela Mayero Florian Faissole et al.
    2.1.0
    LGPL-3.0-or-later
    Used by 2 other packages
    27 Nov 2025