There was a discussion in https://groups.google.com/g/metamath/c/UwTUuNPgaB0/m/NdWefzG4AgAJ about the indices for words. Currently, the indices for words start with 0, and the proposal to change this was not accepted.
For matrices, however, the things are different: The indices for rows and colums usually start with 1, as Thierry explained, so I agree with Thierry. And having the planned conversion function should dispel any doubt. Alexander On Friday, August 28, 2020 at 9:45:33 AM UTC+2 Thierry Arnoux wrote: > 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 a11 (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/477f9d1c-39c4-4c4d-880b-0a9298432112n%40googlegroups.com.
