Thanks Mario! I will dig in that direction and hopefully will make a PR for gsumwsN and amgmN for N=3..8 \o/
-stan On Wed, Sep 9, 2020 at 4:12 AM Mario Carneiro <[email protected]> wrote: > > > On Tue, Sep 8, 2020 at 3:46 PM 'Stanislas Polu' via Metamath > <[email protected]> wrote: >> >> I was expecting to find something along the very broad lines of: >> >> ``` >> ( CCfld gsum { { 1 , A } , { 1 , B } , { 1 , C } } ) = ( ( CCfld gsum >> { { 1 , A } , { 1 , B } } ) + ( CCfld gsum { { 1 , C } } ) ) >> ``` > > > Well, in the first place the statement is false, and a bit not well typed. > The right argument of gsum is a finitely supported function, which is a set > of ordered pairs, which means (1) you should use <. 1 , A >. for the points, > and (2) the domain values should be distinct or it's not a function; that is, > instead of { <. 1 , A >. , <. 1 , B >. , <. 1 , C >. } you should have { <. 1 > , A >. , <. 2 , B >. , <. 3 , C >. }.The easiest way to construct finite > functions on integers like this is using df-word, as in <" A B C ">, and the > relevant lemmas for manipulating such expressions are gsumws1 and gsumccat, > also specialized to gsumccatsn and gsumws2 (it might be good to fill out the > matrix here and prove gsumwsN for n = 3..8). > > Mario > > -- > 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/CAFXXJSudhyg1zSUqiTspDwgoGoQ5wmBYBPuRf_xHPmsrnjzYgA%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/CACZd_0zK%3D9kK_0g_XUX-yHpQ2ypYstm7Ou7JL%2BsXLj2ca248%3DQ%40mail.gmail.com.
