Home Original page

Mathematical Components

  • math-comp/math-comp’s past year of commit activity

  • hierarchy-builder Public

    High level commands to declare a hierarchy based on packed classes

    math-comp/hierarchy-builder’s past year of commit activity

  • analysis Public

    Mathematical Components compliant Analysis Library

    math-comp/analysis’s past year of commit activity

    Rocq Prover

    240 65 94 59

    Updated Apr 15, 2026

  • multinomials Public

    Multinomials for the Mathematical Components library.

    math-comp/multinomials’s past year of commit activity

  • odd-order Public

    The formal proof of the Odd Order Theorem

    math-comp/odd-order’s past year of commit activity

    Rocq Prover

    37 16 1 2

    Updated Apr 13, 2026

  • algebra-tactics Public

    Ring, field, lra, nra, and psatz tactics for Mathematical Components

    math-comp/algebra-tactics’s past year of commit activity

  • finmap Public

    Finite sets, finite maps, multisets and generic sets

    math-comp/finmap’s past year of commit activity

    Rocq Prover

    51 29 12 4

    Updated Apr 1, 2026

  • bigenough Public

    Asymptotic reasoning with bigenough

    math-comp/bigenough’s past year of commit activity

    Rocq Prover

    5 5 0 0

    Updated Mar 26, 2026

  • math-comp/real-closed’s past year of commit activity

    Rocq Prover

    14 12 6 1

    Updated Mar 26, 2026

  • mczify Public

    Micromega tactics for Mathematical Components

    math-comp/mczify’s past year of commit activity