I’ve done a mock-up of this conversion (including index translation), you can find it here: http://us2.metamath.org:88/mpeuni/lmat22e11.html
On the other hand, does any one have any idea or suggestion about how I could have expressed the Laplace expansion without integer indices, on any finite set index? > Le 2 sept. 2020 à 18:54, Mario Carneiro <[email protected]> a écrit : > > > Note that an expression such as <" <" A B C "> <" D E F "> <" G H I "> "> has > the type (0..^N) -> ((0..^N) -> R), which would have to be converted anyway > to match the expected I x I -> R type used by square matrices. If we take I > to be (0..^N) then this is just an uncurry, but if the official index set for > matrices is instead (1...N) then the index remapping could be performed at > the same time. > >> On Wed, Sep 2, 2020 at 5:17 AM 'Alexander van der Vekens' via Metamath >> <[email protected]> wrote: >> For clarification: there is already a definition of (square) matrices based >> on arbitrary finite sets used as index sets (see ~df-mat, contributed by >> Stefan O'Rear). The theorems which I needed to proof Cramer's rule are based >> on this definion. If I understand Thierry correctly, he does not want to >> replace this definition, but to provide an additional, more specialized >> definition with an ordered index set, which can be used for special theorems >> like the Laplace expansion (I was not able to prove it for arbitrary finite >> sets...). >> >> The column vectors which I used for the matrix vector multiplication >> `maVecMul` are also indexed by arbitrary finite sets, as mentioned by >> Thierry, so this also covers the general case Mario is asking for. >> >> - >> Alexander >> >>> On Wednesday, September 2, 2020 at 9:49:50 AM UTC+2 Thierry Arnoux wrote: >>> Indeed, we do have matrix vector multiplication, ` maVecMul `, introduced >>> by Alexander, and used in his proof of Cramer's rule. >>> That operation considers vectors as functions of a single variable, indexed >>> by any finite set. >>> >>> This can only identify with Words (` Word X `, which can be input as ` <" A >>> B C "> ` ) if that set is of the form ` ( 0 ..^ N ) ` ... >>> >>> _ >>> Thierry >>> >>> >>> >>> On 02/09/2020 15:15, Mario Carneiro wrote: >>>> I will reiterate my suggestion to use finite sets for indexing when >>>> possible, which sidesteps the question, but while I would like to defer to >>>> Norm here, I really think a lack of consistency is going to cause actual >>>> problems in this area. What is the definition of a matrix multiplied by a >>>> vector? Surely the vector has to be using the same indexing as the matrix. >>>> Perhaps we can have a separate type for vectors than words, but this seems >>>> superfluous and repetitive. >>>> >>>> I am willing to defer to decisions on convention making but I would like >>>> to see some clear path forward for the main definitions here and how they >>>> are not better served by a minor variation on the definition such as >>>> reindexing. >>>> >>>> Mario >>>> >>>> On Wed, Sep 2, 2020 at 12:30 AM Thierry Arnoux <[email protected]> wrote: >>>>> Thanks for all feedback! >>>>> >>>>> There are valid arguments on both sides, so we need Norm or Mario to do a >>>>> final call. >>>>> >>>>> >>>>> >>>>>> On 29/08/2020 08:06, Norman Megill wrote: >>>>>> While I'm not an expert, my guess is that the major uses of 0-based >>>>>> arrays are in computer science and some computer programming languages, >>>>>> where they can offer an advantage for some algorithms. >>>>>> >>>>>> But mathematics is meant for humans, and humans tend to count from 1. >>>>>> That's why we number the proof steps on our web pages starting with 1. >>>>>> Having the "first" step numbered with 0 would seem unnatural to me. >>>>>> >>>>>> As AV pointed out, we haven't been able to find a linear algebra >>>>>> textbook with matrices numbered from 0. On Wikipedia, there are 4 >>>>>> subtopics listed under >>>>>> https://en.wikipedia.org/wiki/Vector#Mathematics_and_physics which are: >>>>>> >>>>>> https://en.wikipedia.org/wiki/Euclidean_vector >>>>>> https://en.wikipedia.org/wiki/Row_and_column_vectors >>>>>> https://en.wikipedia.org/wiki/Vector_space >>>>>> https://en.wikipedia.org/wiki/Vector_field >>>>>> >>>>>> These all show 1-based indices. >>>>>> >>>>>> I have always wanted to see set.mm to be as close to mathematical >>>>>> literature as possible or practical. Apparently almost all of linear >>>>>> algebra literature uses 1-based matrices and vectors, so I think that is >>>>>> what set.mm should do. Even if for some purposes it would be more >>>>>> convenient to have matrices 0-based, it hasn't seemed to have harmed the >>>>>> field. >>>>>> >>>>>> My vote is to conform to the literature and have matrices and vectors >>>>>> 1-based. >>>>>> >>>>>> On Friday, August 28, 2020 at 2:20:35 PM UTC-4 di.... gmail.com wrote: >>>>>>> My vote is also in favor of starting with 0, or even better, doing >>>>>>> everything over generic finite sets when possible and falling back on ( >>>>>>> 0 ..^ N ). I realize that close correspondence with papers is >>>>>>> considered important here but mathematicians write for their own ease. >>>>>>> In a math paper, you can write either a_0, ..., a_(n-1) or a_1, ..., >>>>>>> a_n - which is easier? Besides the strictness of a few inequalities >>>>>>> this is probably the only difference, so a_1, ..., a_n is preferred >>>>>>> because it is very slightly shorter. >>>>>>> >>>>>>> In formalization, we should also write for our own ease. In this case, >>>>>>> that means better interfacing with the theory of finite words, which >>>>>>> uses ( 0 ..^ N ). There are also other reasons to prefer 0 based >>>>>>> indexing but in this case I think consistency with words (viewed as 1D >>>>>>> vectors) is more important than that. >>>>>>> >>>>>>> On Fri, Aug 28, 2020 at 1:43 PM Benoit wrote: >>>>>>>> I'm still in favor of words starting at 0. As for matrix rows and >>>>>>>> columns, it would be more...wait for it... natural to start at 0, but >>>>>>>> since the literature overwhelmingly prefers to start at 1, maybe it's >>>>>>>> better to conform with it (there are a few "historical accidents" like >>>>>>>> that, for instance defining \pi as half what it should be, and since >>>>>>>> the consequences are very mild, it stays like that). >>>>>>>> And to state the obvious: since most results using the fact that rows >>>>>>>> and columns are natural numbers have them intervene in the form >>>>>>>> (-1)^{i+j}, shifting both row and column indices by 1 does not change >>>>>>>> the parity of the sum, so these statements are unaffected. >>>>>>>> >>>>>>>> Benoit >>>>>>>> >>>>>>>> On Friday, August 28, 2020 at 6:14:57 PM UTC+2 Alexander van der >>>>>>>> Vekens wrote: >>>>>>>>> >>>>>>>>> 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/7eeabd5a-29c3-431b-aaba-87f457827d53n%40googlegroups.com. >>>>> -- >>>>> 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/d605c6c1-20ff-3b46-228b-4645c704db08%40gmx.net. >>>> -- >>>> 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/CAFXXJSspwoKtV5cGUwenJJ4MF4js-a_mzhVyi-7vi9KAkkJKRw%40mail.gmail.com. >> >> -- >> 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/d5e41385-2659-49b1-8176-011144637d9dn%40googlegroups.com. > > -- > 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/CAFXXJSvm%3D0YNAOj_ZF8XBvuoWbfaTEHVsymViqGnX0czV6tHhw%40mail.gmail.com. -- 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/1F73E402-F4BB-4446-9AA6-D0C287C40186%40gmx.net.
