I think that removing dependence on AC is usually a good thing. Norm
On Friday, May 14, 2021 at 4:14:24 AM UTC-4 tbrend...@gmail.com wrote: > 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4df78adb-d73f-421c-814d-fe78748bfa83n%40googlegroups.com.
