Skip to content
@math-comp

Mathematical Components

Pinned Loading

  1. math-comp math-comp Public

    Mathematical Components

    Rocq Prover 670 128

Repositories

Showing 10 of 27 repositories
  • analysis Public

    Mathematical Components compliant Analysis Library

    math-comp/analysis’s past year of commit activity
    Rocq Prover 238 65 91 58 Updated Mar 13, 2026
  • hierarchy-builder Public

    High level commands to declare a hierarchy based on packed classes

    math-comp/hierarchy-builder’s past year of commit activity
    Rocq Prover 104 MIT 28 90 (1 issue needs help) 24 Updated Mar 13, 2026
  • math-comp Public

    Mathematical Components

    math-comp/math-comp’s past year of commit activity
    Rocq Prover 670 128 130 41 Updated Mar 13, 2026
  • trajectories Public
    math-comp/trajectories’s past year of commit activity
    Rocq Prover 0 5 8 0 Updated Mar 12, 2026
  • 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 Mar 6, 2026
  • Abel Public

    A proof of Abel-Ruffini theorem.

    math-comp/Abel’s past year of commit activity
    Rocq Prover 30 8 1 10 Updated Mar 6, 2026
  • algebra-tactics Public

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

    math-comp/algebra-tactics’s past year of commit activity
    Rocq Prover 38 4 14 (1 issue needs help) 0 Updated Mar 3, 2026
  • mczify Public

    Micromega tactics for Mathematical Components

    math-comp/mczify’s past year of commit activity
    Rocq Prover 28 9 4 (1 issue needs help) 1 Updated Mar 3, 2026
  • 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 Mar 3, 2026
  • real-closed Public

    Theorems for Real Closed Fields

    math-comp/real-closed’s past year of commit activity
    Rocq Prover 14 12 6 2 Updated Mar 3, 2026
View all repositories