Planning to change mreexexd in main database.

[tbrend...@gmail.com]

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?

[Norman Megill]

I think that removing dependence on AC is usually a good thing.

Norm

[Benoit]

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

[David A. Wheeler]

> On May 14, 2021, at 8:17 AM, Norman Megill <n...@alum.mit.edu> wrote:
>
> I think that removing dependence on AC is usually a good thing.

I agree.

If the proof is much more complex without AC, I think it can be a good idea to keep the original “simpler” proof as ALT proof. In that case, I strongly recommend noting *WHY* this is being kept, in this case, because using AC makes it “much simpler” to prove.

--- David A. Wheeler