[Metamath] metamath.exe - added "/extract" to "write source"

2020-09-04 Thread Norman Megill
The amount of material in set.mm has grown quite large and may be overwhelming for someone who just wants to see what is needed to prove a particular theorem of interest. Organizing set.mm with section headings and splitting it into modules help but only partially address the problem. "show

Re: [Metamath] Re: Matrix indexing start

2020-09-04 Thread 'fl' via Metamath
> Apparently essentially 100% of linear algebra textbooks start at 1. > Well I think there is now a consensus in the use of matrices, tuples and words. -- FL -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group