More Z/nZ theorems in iset.mm #4962
Open
+587
−166
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Stated as in set.mm. The proof needs intuitionizing in various places but is similar to the set.mm proof.
Includes a note about how to intuitionize one part of the proof.
Stated as in set.mm. The proof is the same as the set.mm proof with some changes for set existence.
Stated as in set.mm. The proof is the set.mm one with some changes to use ringcl in place of ovex .
Stated as in set.mm. The proof needs a fair number of changes for set existence but is otherwise the set.mm proof.
Stated as in set.mm. The proof is fairly different from the set.mm proof but the needed set existence steps can be added without changing the conclusion.
Turns out there is a trick which lets us prove this without the set existence condition found in 2idlvalg . Document this trick in mmil.html (not the first time iset.mm has used it, but worth a mention as it comes up from time to time and might not be obvious). Move 2idlmex slightly earlier in the file so we can use it in this proof.
Stated as in set.mm. The iset.mm proof is a new one. It does have to go through a number of steps, perhaps non-obvious ones, but it is possible to prove the theorem as stated as in set.mm.
Stated as in set.mm. The proof is the set.mm proof with some small changes around set existence.
Stated as in set.mm. The proof is the set.mm proof but is expanded because a number of additional steps are needed for set existence.
Stated as in set.mm. The proof needs several additional steps for set existence but is otherwise the set.mm proof.
This rename has already been done in set.mm.
Stated as in set.mm. The proof is basically the set.mm proof but requires adjustment for differences in extensible structure theorems.
Point to the closest replacement we have so far.
Stated as in set.mm. The proof is the set.mm proof with small changes for set existence.
This is raleqtrdv , rexeqtrdv , raleqtrrdv , and rexeqtrrdv .
Stated as in set.mm. The proof is the set.mm proof except: * some changes to express that the proposition in the if statement is decidable * modulus theorems take rationals rather than reals (but in this case it is an integer, so this is an easy change)
Stated as in set.mm. The proof is the set.mm proof except that it needs a few changes for set existence.
Stated as in set.mm. The proof is the set.mm proof but needs some intuitionizing in a number of places.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is
znzrh2throughznhashand a bunch of theorems (mostly homomorphism theorems) which are used by those proofs.