I don't understand what you mean by "replacing the intersection of cardinalities with an if statement", but if it's a change of the proof that removes dependency on ax-ac2, this is of course welcome. You can: * copy mreexexd to mreexexdOLD, with comment "Obsolete proof of ~ mreexexd . (Proof modification is discouraged.) (New usage is discouraged.)" (and place it right after mreexexd) * modify the proof of mreexexd as you indicated, and add at the end of its comment: "Revised to remove dependendy on ~ ax-ac2 . (Revised by xxx, 14-May-2021.)"
Benoît On Friday, May 14, 2021 at 2:17:09 PM UTC+2 Norman Megill wrote: > 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 [email protected] 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/a2799725-9d2d-4855-9f51-1afb6303c3ddn%40googlegroups.com.
