package rocq-num-analysis-algebra
Algebraic structures for numerical analysis in Rocq
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-num-analysis-2.2.0.tar.gz
sha512=d1996546d967000045e3c58484d6bda8bf4e153f62d6ee42789090c772f0fede197a41b22cfd8253c2729cec515d0bb834d52904d9a38e656858ee7778aac779
Description
This library is based on Coquelicot and provides additional support about commutative monoids, Abelian groups, rings, module spaces, and affine spaces. This includes support for functions to a given algebraic structure, iterated operations (sum, linear combination, barycenter), morphisms, algebraic substructures, and the specific case of finite dimension. It is based on classical logic.
Tags
category:Mathematics/Algebra date:2026-03 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 coefficientPublished: 13 Mar 2026
Dependencies (6)
-
rocq-num-analysis-subset
= version -
coq-coquelicot
>= "3.4" & < "3.5~" - rocq-stdlib
-
rocq-core
>= "9.0" & < "9.2~" - coq-stdlib
-
coq-core
>= "8.20" & < "8.21~"
Dev Dependencies
None
Used by (2)
-
rocq-num-analysis-fem
>= "2.2.0" -
rocq-num-analysis-lax-milgram
>= "2.2.0"
Conflicts
None
On This Page