The most similar case I know to this is the definition of polynomials (df-mpl) as a subset of power series (df-psr). In that case, I anticipated that we would not care so much about power series, so df-mpl itself defines a substructure, but the subset is also accessible using "the base set of polynomials" which is a subset of the set of power series, and theorem mplval2 supports this way of writing it.
My guess for this case is that it is more useful to have diagonal matrices be a subring (i.e. a subset about which you prove closure properties) rather than a freestanding structure. You still get most of the algebraic benefits with it being a subring, but this retains the connection between the two structures. Similar remarks apply to the orthogonal and special linear groups, although in these cases you will also want easy access to the group itself. Mario On Wed, Dec 18, 2019 at 12:16 PM Norman Megill <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/2ca0041c-fdf7-4bab-ad67-9fc7557a6e04%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSudkuc9%2BHp%3D_7Nq%3DQKNGiTBTP2ugVR7pvDKAOjVMVFMEw%40mail.gmail.com.
