Hi all, I recently formalized a proof of the Laplace expansion of determinants (~ mdetlap), which I think would be useful to pull to the main part of set.mm. Because the formula makes calculation based on the row and column indices of the element of the matrix, I'm using matrix with integer indices (in contrast with the rest of the development on matrices which is based on arbitrary sets).
I chose indices in ` ( 1 ... N ) ` , so that the top-left matrix element is a_11 (in set.mm written ` ( 1 A 1 ) ` ). It seems using indices starting from one is the convention used for mathematics, I have not found yet a reference with indices starting at zero (and neither did Norm), however we would like to run this through the community. Most programming languages start indices with zero, with the exception of R and several others. In set.mm words indices start with zero. What's your opinion? Should matrix indices start with one or zero? Thanks for your input! BR, _ Thierry PS. I would later like to define a "literal" matrix function which would be used like this to transform words (for any matrix size up to 8x8) into matrices : ( litMat ` <" <" A B C "> <" D E F "> <" G H I "> "> ) This would allow a bridge/conversion. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/6743fef1-ad67-d415-9377-b45f257005d4%40gmx.net.
