> > Would you mind proposing the additional text for the comments to those > definitions? >
I wouldn't mind. Will you keep on with the direct sum or will you use the product Xs directly? The direct product would remove one layer. It woulld be less complex. I cite wilipedia: "In the case of two summands, or any finite number of summands, the direct sum is the same as the direct product <https://en.wikipedia.org/wiki/Direct_product>." https://en.wikipedia.org/wiki/Direct_sum I can then help doing the actual changes in set.mm if needed. > > I will send them to you. -- FL -- 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/ee03feaf-70b8-4283-89c3-ee3b4efdfacc%40googlegroups.com.
