Stream: math-comp users

Topic: Reshaping matrix


view this post on Zulip Julin Shaji (Oct 28 2023 at 17:35):

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?

view this post on Zulip Pierre Roux (Oct 28 2023 at 17:46):

castmx if for the case r1 = r2 and c1 = c2 I guess

view this post on Zulip Julin Shaji (Oct 28 2023 at 17:51):

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_mxfunction for which I wanted to make some easy examples to compare with.

view this post on Zulip Julin Shaji (Oct 28 2023 at 17:51):

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.

view this post on Zulip Pierre Roux (Oct 28 2023 at 18:51):

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


Last updated: Jul 23 2024 at 21:01 UTC