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/c5d3d18d-c69e-491b-a721-952fc79dda6c%40googlegroups.com.
