Hello! I am looking for information about math-comp type VectType (for finite-dimensional vector space)

1) Is there information other than https://math-comp.github.io/htmldoc_1_12_0/mathcomp.algebra.vector.html ?

2) Are there bijections from and to different VectTypes when their dimension is equal?

3) Is there a proof that polynomials of a given degree (smaller than n) form a VectType?

Thanks!

Sylvie Boldo said:

Hello! I am looking for information about math-comp type VectType (for finite-dimensional vector space)

1) Is there information other than https://math-comp.github.io/htmldoc_1_12_0/mathcomp.algebra.vector.html ?

I don't think there is another doc, no.

2) Are there bijections from and to different VectTypes when their dimension is equal?

I'm not aware of such a contribution. It wouldn't be too hard to add though, I could do it or guide anyone trying to do it.

3) Is there a proof that polynomials of a given degree (smaller than n) form a VectType?

There is this old PR which should be refreshed and merged.

I suggest to define:

```
Definition vspace_fun {vT vT' : vectType} (U : {vspace vT}) (V : {vspace vT'}) (v : vT) :=
\sum_(i < \dim U) coord (vbasis U) i v *: (vbasis V)`_i
```

And prove stuff like:

```
Lemma vspace_fun (vT vT' : vectType) (U : {vspace vT}) (V : {vspace vT'}) : (U <= V)%VS
cancel (vspace_fun U V) (vspace_fun V U).
Proof. ... Admitted.
```

and

```
Lemma vspace_is_linear (vT vT' : vectType) (U : {vspace vT}) (V : {vspace vT'}) :
linear (vspace_fun U V).
Proof. ... Admitted.
Canonical vspace_fun_linear (vT vT' : vectType) (U : {vspace vT}) (V : {vspace vT'}) :=
Linear (vspace_is_linear U V).
```

Thanks! I'll have a look at all that.

(U <= V)%VS was not typing indeed. I also changed it to (\dim U <= \dim V)%nat :-)

But I have problems proving the cancel property on vspace_fun as it seems to require that v \in U. Did I miss something?

Last updated: Jan 29 2023 at 19:02 UTC