Jake Zweifler (Oct 06 2022 at 01:35): Jake Zweifler (Oct 06 2022 at 01:35):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!
Pierre Roux (Oct 06 2022 at 05:52):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).
Karl Palmskog (Oct 06 2022 at 07:20):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