> > > I know I keep harping on not wanting to add a catalog of definitions (with > shallow theorems) that are otherwise unused, but it has been done in the > past with the work essentially wasted, sometimes causing resentment, and I > want to avoid that. >
I just don't see how a "catalog" of definitions could cause resentment because as far as I know the definitions have always been carefully kept in the mathboxes. Funny explanation where one gives as a cause of something one has always wanted, something which has never existed. And to be honest we have never given a "catalog" of definitions. The definitions in the topology part were useful and used to prove theorems contrary to what you say. Those in the algebra part were useful too. The rare ones that are useless can be easily removed since they ere not used. As far as I remember, you didn't want the definition of module. I insisted to keep it. It is perhaps the resentment you are speaking of. But in that case it is yours. I just don't understand why you make such a fuss over the definition of a module. It is in use in current mathematics. If the extensible structures must only be reduced to the chain "group - ring - vector space " I think they are not very exensible. But if you insist we can just stop using the extensible structure. -- 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/3dbf7415-0c2d-4237-96d8-966c3da3657c%40googlegroups.com.
