Intuitionize Ring and CRing up until iscrngd #4540
Conversation
~ringi was deleted - why not making it a lemma ~ringdilem like ~srgdilem in #4522? |
What I said in the commit message was:
But I guess it doesn't really matter much to me one way or the other 🤷 . I'll bring back |
This is the syntax , df-ring , and df-cring . Copied without change from set.mm.
Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof.
Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof.
Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof.
Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof.
Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof.
Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof.
This is ringdilem , ringdi , and ringdir . Copied without change from set.mm.
Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof.
Includes lemma ringidmlem , which is stated as in set.mm. Its proof needs some intuitionizing but is basically the set.mm proof. ringlidm and ringridm are copied without change from set.mm.
Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof.
Copied from set.mm, with the only change being to the comment, to remove a reference to a theorem iset.mm doesn't have yet.
Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof.
Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof.
Stated as in set.mm. The proof needs a small amount of intuitionizing but is basically the set.mm proof.
Stated as in set.mm. The proof needs a little bit of intuitionizing but is basically the set.mm proof.
|
I have added the change to keep |
The proof does not consist of two separate parts which are joined at the end via ~jca (step 22): the common part starts at step 16! Therefore, I think the existence of ~ringdilem ist justified. |
Yeah, after I wrote that I took a closer look and I'd agree that the common part is a bit bigger than I had thought. Whether 16 steps is big or small in the grand scheme of things is why this is a bit of a 🤷 for me, but we've already decided to keep the lemma, so we'll do that. |
This is the first part of the rather long section "Definition and basic properties of unital rings".
Most of the intuitionizing is pretty straightforward #4495 style set existence changes.
The one change to set.mm was inspired by #4522 (comment)