An Introduction to MathComp-Analysis

staff.aist.go.jpsite

Lecture notes on getting started with the Mathematical Components library and using it for classical reasoning and real analysis.

from

Coq

added

2026-10-10

likes

0

similar

1. ▲
   Analysis github.com

   tool category #coq link ↗

   Library for classical real analysis compatible with Mathematical Components.

2. ▲
   Mathematical Components math-comp.github.io

   site category #coq link ↗

   Formalization of mathematical theories, focusing in particular on group theory.

3. ▲
   Mathematical Components wiki github.com

   site category #coq link ↗
4. ▲
   The Mathematical Components book math-comp.github.io

   site category #coq link ↗

   Book oriented towards mathematically inclined users, focusing on the Mathematical Components library and the SSReflect proof language.

5. ▲
   MathComp Extra github.com

   tool category #coq link ↗

   Extra material for the Mathematical Components library, including the AKS primality test and RSA encryption and decryption.

6. ▲
   MathComp Tutorial Materials github.com

   tool category #coq link ↗

   Source code for Mathematical Components tutorials.

Coq › Resources > Course Material: “Lecture notes on getting started with the Mathematical Components library and using it for classical reasoning and real analysis.”