Hi Thierry,
I actually think we should reference the names of the variables, give their
real type when V has been used (for example for i in the case of df-rrx,
or for r and i in the case of df-frlm, or for s and r in the case of
df-dsmm), and finally delete the definitions that are useless (this is the
case of df-rrx I think).
Using a direct sum when the number of dimensions is finite seems to me to
add unnecessary complexity (or it should be said in the commentary
that in this case the finite support is useless and that df-dsmm is only
used for the sake of not having an additional definition).
It is also necessary to explain in what order this is done. I think that
adding the sequence of actions is very enlightening:
1) building the RR field
2) building the module from the field
3) building a function indexed by naturals (𝑖 × { {(ringLMod'𝑟)})
4) making the tuples of the base set of the product and making the
pointwise operations,the distance, topology and Hermitian form.
5) and finally making and adding the norm.
It's also not bad to add at *which level* of definition the elements are
built and add to the structure, for example
Hermitian form at the df-prds level but the norm at the tiCHil level.
By the way, I wondered if all your metric and topological structures are
correctly connected.
And we have to comment on df-prds. In particular, explain that this
operator only looks so strange because his real purpose is to overload a
symbol.
--
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/0d224e39-75a4-4cd9-94d3-7ce938629608%40googlegroups.com.
