## Stream: math-comp users

### Topic: About vectType

#### Sylvie Boldo (May 03 2022 at 11:17):

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!

#### Cyril Cohen (May 03 2022 at 12:02):

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.

#### Cyril Cohen (May 03 2022 at 12:17):

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).


and

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

#### Sylvie Boldo (May 03 2022 at 12:31):

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

#### Sylvie Boldo (May 03 2022 at 14:25):

(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