Add sigma (df-sgm) to iset.mm #5049
Merged
+582
−183
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
This is the sigma syntax and df-sgm . Copied without change from set.mm.
A natural number has finitely many divisors. The proof is taken from a portion of the phisum proof. Shorten the phisum proof using dvdsfi .
Stated as in set.mm. The proof is the set.mm proof with changes needed to use fsumcl instead of sumex .
Stated as in set.mm. The proof is the set.mm with a small change for differences in ^c theorems.
Stated as in set.mm. The proof is the set.mm proof with small changes related to differences in finite set theorems.
Stated as in set.mm. The proof is the set.mm proof with some small changes for differences in finiteness and ^c theorems.
Stated as in set.mm. The proof is the set.mm proof with small changes around theorems related to finiteness and nonempty sets.
This is cxpmul2 from set.mm but where the base has to be a positive real, not any complex number. The proof is based on a portion of the set.mm proof although most steps need some changes.
Deduction form of rpcxpmul2 .
Stated as in set.mm. The proof is the set.mm proof with some small changes related to set existence and differences in ^c theorems.
Stated as in set.mm. The proof is the set.mm with a few small changes to account for differences in finite set theorems.
Stated as in set.mm. The proof is the set.mm proof with a small change for differences in ^c theorems.
Stated as in set.mm. The proof is the set.mm proof with several changes for differences in ^c theorems and changing not equal to apart.
Stated as in set.mm. The proof is the set.mm proof with a few changes for set existence and apartness vs not equal.
Stated as in set.mm. The proof is the set.mm proof with changes for finite set theorems and set existence. In some parts of the proof the changes are significant but some parts of the proof, and the overall logic, are unchanged.
Stated as in set.mm. The proof is the set.mm with small changes for differences in ^c theorems.
avekens
reviewed
Oct 17, 2025
avekens
reviewed
Oct 17, 2025
avekens
reviewed
Oct 17, 2025
avekens
reviewed
Oct 17, 2025
Although the proof is shorter than in iset.mm it seems like this may be useful. Use it to shorten several proofs.
It isn't clear what "prime count" was supposed to mean here; hopefully "exponent" (of the prime power) is clearer.
The change is to say "nonnegative integer" rather than "integer". The theorem had already said NN0 rather than ZZ . This is cxpmul2 and cxpmul2d in set.mm and rpcxpmul2 and rpcxpmul2d in iset.mm.
avekens
approved these changes
Oct 18, 2025
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
The definition and the theorems intuitionize without a lot of trouble.
Includes a few additions to
^ctheorems.Includes
dvdsfi(a natural number has finitely many divisors), extracted from a portion of thephisumproof.