The Metamath -> MM0 importer already contains a feature for selecting which
target theorems you want, so it has the same effect as using /extract on
the source database first and then importing it. I've been using numbers
for example theorems like dirith or pnt in my talks. I wonder what is the
On Saturday, September 5, 2020 at 2:46:44 AM UTC-4 Alexander van der Vekens
wrote:
> That's sound really great! I will try this new feature soon, using the
> friendship theorem as "root"...
>
Good choice. I was curious so I added it (temporarily) here:
> In metamath version 0.192 ( http://us2.metamath.org/index.html#mmprog ),
"write source" has a new qualifier, "/extract ",
> which will create a self-contained database containing exactly and only
the axioms and theorems needed to prove
> A possible use for this is to create a miniature
In any case, dissociating the treatment of matrices, tuples and words is a
bad idea.
--
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
> I think there is no consensus to use index sets starting with 1,
> especially not for tuples/words (actually, there was a consensus to start
> with 0 for words, see discussion in
> https://groups.google.com/g/metamath/c/UwTUuNPgaB0/m/NdWefzG4AgAJ).
There has never been any consensus
Regarding the Laplace expansion more specifically:
I assume that a determinant is defined over matrices M : A x A -> R, where
A is a finite (unordered) set. Suppose we wish to perform cofactor
expansion along row i e. A. The j'th cofactor (where j e. A) is given by
the elements of M on (A\{i}) x
I do not have strong opinions on this issue and I will not be the one to
do the work, but I still think "starting at 0" for matrices is more
natural. Of course, the more important thing is to have as many results as
possible stated for arbitrary finite sets (or even arbitrary sets for some
That's sound really great! I will try this new feature soon, using the
friendship theorem as "root"...
--
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
As proposed by FL in
https://groups.google.com/g/metamath/c/n5g69qfwBmE/m/McJAgtdSAgAJ, the
additional assumption that the finite index sets are totally orderer should
be sufficient to express and prove the Laplace expansion. Regarding the
expression ` -1 ^ ( i + j ) ` , a special concept of
I think there is no consensus to use index sets starting with 1,
especially not for tuples/words (actually, there was a consensus to start
with 0 for words, see discussion in
https://groups.google.com/g/metamath/c/UwTUuNPgaB0/m/NdWefzG4AgAJ).
Regarding matrices, I am also in favour of
10 matches
Mail list logo
