Is there a way to 'reshape' a matrix in mathcomp?

ie, given a matrix of dimension `r1 ⨯ c1`

, can we make it `r2 ⨯ c2`

provided that `r1 * c1 == r2 * c2`

?

There's `castmx`

, but is it meant for this purpose?

If I understood anything, it looks a helper function to make proofs involving dependent type easier. Is it so?

`castmx`

if for the case `r1 = r2`

and `c1 = c2`

I guess

But that's not exactly changing the shape, right? Is there a built-in way to reshape it otherwise?

I was thinking of reshaping because I wanted to experiment with `block_mx`

function for which I wanted to make some easy examples to compare with.

Having a way to enumerate all elements in an `ordinal`

and then shaping that into a matrix would be cool as well. That's where I'm headed next.

Maybe mxvec and vec_mx: https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/matrix.v#L107-L110 ?

Last updated: Oct 13 2024 at 01:02 UTC