Stream: math-comp analysis

Topic: Real numbers and realFieldType

view this post on Zulip Pablo (Feb 20 2024 at 16:38):

Hello, I am trying to use the standard real numbers (Require Import Reals) for the definition of a matrix using mathcomp.algebra.matrix.

I am trying to use a library (Coq-Polyhedra) which uses a variable to of type R : realFIeldType to declare different structures using matrixes and vectors. I am trying to instantiate one of these structures, but it requires that the values of the matrix are inside a realFieldType. Is there a way to prove that indeed the Reals are a realFIeldtype as defined in mathcomp.algebra.ssrnum.

Thank you in advance.

view this post on Zulip Quentin VERMANDE (Feb 20 2024 at 16:45):

If I got your question correctly, this is done in mathcomp-analysis, in Rstruct.v.

view this post on Zulip Notification Bot (Feb 20 2024 at 16:49):

This topic was moved here from #Coq users > Real numbers and realFieldType by Karl Palmskog.

view this post on Zulip Karl Palmskog (Feb 20 2024 at 16:52):

Rstruct.v is to my knowledge part of the opam coq-mathcomp-analysis package and should be usable once installed by doing From mathcomp Require Import Rstruct.

Last updated: Jun 25 2024 at 19:01 UTC