Finish intuitionizing section "Groups: Definition and basic properties" #4488
+754
−13
Conversation
This file contains 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
avekens
approved these changes
Dec 26, 2024
|
I'm planning on rebasing this (because a number of changes have been merged since it was created), and then merging if the tests pass. |
Includes syl5bb comment from set.mm.
This is grpinvpropd from set.mm with set existence conditions added. The proof is similar to the set.mm proof.
Stated as in set.mm. The proof needs a small amount of intuitionizing but is basically the set.mm proof.
This is dfgrp3 from set.mm with non-empty changed to inhabited. The proof needs some intuitionizing for that change but is basically the set.mm proof. Includes lemma dfgrp3mlem which is dfgrp3lem from set.mm with a similar change. Minimize dfgrp3 in set.mm.
This is dfgrp3e from set.mm with non-empty changed to inhabited. The proof needs some intuitionizing but is basically the set.mm proof.
Stated as in set.mm. The proof needs a fair bit of intuitionizing around set existence but follows basically the structure of the set.mm proof.
This is grpsubpropd from set.mm with set exixtence hypotheses. The proof needs some intuitionizing but is similar to 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 set.mm proof works intuitionistically but needs minor changes to reflect differences in opelres/opelresi between set.mm and iset.mm.
Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof.
This is prdsinvlem , prdsgrpd , prdsinvgd
This is pwsgrp , pwsinvg , pwssub
This is imasgrp2 , imasgrp , imasgrpf1 .
Copied from set.mm without change. The $d B x $. is not necessary for the proof, but is copied to keep iset.mm consistent with set.mm.
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.
Most of this intuitionizes fairly easily, with the main exception being theorems which refer to concepts which aren't yet developed in iset.mm.