As proposed by FL in https://groups.google.com/g/metamath/c/n5g69qfwBmE/m/McJAgtdSAgAJ, the additional assumption that the finite index sets are totally orderer should be sufficient to express and prove the Laplace expansion. Regarding the expression ` -1 ^ ( i + j ) ` , a special concept of parity must be defined for (finite) totally ordered sets...
On Wednesday, September 2, 2020 at 7:02:23 PM UTC+2 Thierry Arnoux wrote: > On 02/09/2020 23:25, 'fl' via Metamath wrote: > > The best to do is redefine the <" ...>" operator so that it takes (1 ... > N) as its set of indices and then fix up all the proofs referring to the > definition. > You should have only one definition for matrices, tuples and words since > all that is the same story. Or at most two: one with a abstract finite > set of indices and another one with (1... N). > > Like mentioned by Norm in the original thread about index start for words, > I'm afraid that would be a huge work, there are already hundreds of > theorems making use of that range. > That's why I would like to ask the same about matrices now, before writing > more theorems within whichever convention. > > Of course we shall try to use arbitrary sets whenever possible... which > leads me to the other point: > > 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? >> > > The laplace expansion of the determinant (just one level of expansion, not > recursive) requires a choice of row to expand over (which is an element of > the index set), and then it's an unordered finite sum. No integers needed. > > Yes, but what is the factor you apply to each submatrix determinant ? The > textbooks all have ` -1 ^ ( i + j ) ` , where i and j are *integer* > indices. Of course, start index does not matter, but where do those numbers > come from when working with arbitrary sets? > > _ > Thierry > -- 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/fa85e81c-d8f5-4305-ab5f-5987f236d25an%40googlegroups.com.
