Hi Frédéric, We could do two things to make the definition easier to understand:
One thing would be to provide more explanations in the comment for df-ehl, like, explaining that this defines the Euclidean spaces as direct sums of identical copies the field of the real numbers, and pointing to other definitions (where more explanations can also be provided if needed), or pointing to an appropriate reference in the littérature. Another thing would be to expand the different components of the structure, showing what is the “base”, the group addition operation, etc. are what one would expect. Maybe we could also note that the matrix ring is defined in a similar way. About the starting index, I understand your concern. I started with index 0 because but I believe the dimension 0 is an interesting case. This is not Scott Fenton’s convention (he starts at 1 in df-ee), but I think maybe Scott’s definition can be extended without causing too much “damage” (i.e. proofs to be rewritten). I’ll give it a try if I find time to. BR, _ 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/C6A6AFD2-2319-4940-980A-8424D581DB97%40gmx.net.
