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.

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

.

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

`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