Hello,

I am trying to use addmx from mathcomp.algebra.matrix, but ran into the following type mismatch on the arguments I am inputting into the function:

Here, R is just the reals from Coq.Reals because I would like to work with matrices on real numbers. I am wondering if there is some way to specify that the reals are indeed an abelian group, or if there is another more compatible library for reals that I should try instead. I am newer to math-comp and would really appreciate any help or feedback.

You probably need the Rstruct.v file from mathcomp-analysis that provides mathcomp algebraic structures to the reals R from the stdlib.

But if you don't use anything specific to the reals from the stdlib, it could just be as good to use the reals provided by mathcomp analysis itself.

Indeed, as Pierre explained, the type for addmx is:

```
addmx : forall [V : nmodType] [m n : nat], 'M[V]_(m, n) -> 'M[V]_(m, n) -> 'M[V]_(m, n)
```

thus, you need to have in scope the instance so Coq knows that `R`

is a `nmodType`

.

(Note a bug in printing `addmx`

type in Coq 8.19)

Last updated: Jul 25 2024 at 16:02 UTC