You might've already noticed when I posted my first attempt to prove that the algebraic numbers were a field, but I made a minor change to the proof of mreexexd that would make it cease to be reliant on ax-ac2 (replacing the intersection of cardinalities with an if statement) and I was going to make that change to the main database on my next upload, which is going to be a theorem that a matrix on a field is a unit iff the determinant is non-zero. I was wondering if this would be okay?
-- 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/25fef5f0-5612-42ec-892c-fcc0a963f821n%40googlegroups.com.
