I looked this over but haven't formed a strong opinion one way or the other. So if you prefer to use a set instead of a structure for this application, it is acceptable to me.
Norm On Wednesday, December 18, 2019 at 1:32:19 AM UTC-5, Alexander van der Vekens wrote: > > Thierry posted the follwing in GitHub: > > I think my vote may go to your current ‘ DMatALT ‘, since its definition >> is simpler, the operations are identical, and I would assume that later >> developments would use more often statements like “M is a diagonal matrix” >> rather than “the set of diagonal matrices forms a ring”. >> > > I think these are good arguments for defining substructures as sets (and > not structures). Meanwhile, I would also prefer these definitions (DMatALT, > ScMatALT), because they better fit to the way substructures are currently > used in set.mm. Furthermore, it will be easier to revise the existing > theorems about diagonal/scalar matrices, because they are based on the > set-like definitions already. > > If nobody has arguments for a structure-like definition, I will switch the > names of the definitions (ALT vs. non-ALT) and start to revise the theorems > about diagonal/scalar matrices using the set-like definitions. > > Alexander > -- 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/2ca0041c-fdf7-4bab-ad67-9fc7557a6e04%40googlegroups.com.
