Hello! Does anyone know of any more advanced number theory/algebra libraries in Coq? Specifically, one that defines quotient rings and more advanced subsets of C such as Z[sqrt(2)]? I am trying to prove some facts about matrices over Z[1/sqrt(2), i] and (Z/2Z)[1/sqrt(2), i]. Note that I am using Coquelicot's complex numbers which are represented as ordered pairs (R, R). My idea is to have a separate type represent these sets, but there could also be a predicate that returns true for complex numbers that are members of Z[1/sqrt(2), i]. But then how should I define Z/2Z and more generally Z/nZ? Does anyone have any suggestions? Thanks so much!

I don't know if that would fit you need but MathComp (hence MathComp Analysis) has more algebra, and machinery for quotients, than the stdlib (and Coquelicot).

there is https://depot.lipn.univ-paris13.fr/mayero/coq-num-analysis that uses Coquelicot, but I guess it's not exactly chock-full of algebra. (`coq-num-analysis`

package in opam)

Last updated: Oct 05 2023 at 02:01 UTC