Skip to content

Add lgseisenlem4 to iset.mm #5010

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 21 commits into from
Sep 14, 2025
+533 −16
Merged

Add lgseisenlem4 to iset.mm #5010

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
5940ce1
add gsumzsubmcl to mmil.html
jkingdon Sep 6, 2025
6f3381c
add gsumsubgcl to mmil.html
jkingdon Sep 6, 2025
b2e83a0
add gsumzaddlem , gsumzadd , gsumadd to mmil.html
jkingdon Sep 7, 2025
0eb720e
add gsummptfsadd to mmil.html
jkingdon Sep 7, 2025
bb31fcd
add gsum split theorems to mmil.html
jkingdon Sep 7, 2025
b6763e6
Add gsumfzconst to iset.mm
jkingdon Sep 8, 2025
0aecacb
add gsumconstf to mmil.html
jkingdon Sep 9, 2025
8fb1ad3
add gsummptshft to mmil.html
jkingdon Sep 9, 2025
8cee88f
Add gsumfzmhm to iset.mm
jkingdon Sep 9, 2025
828791d
Add gsumfzmhm2 to iset.mm
jkingdon Sep 9, 2025
17fab44
Add gsumfzconstf to iset.mm
jkingdon Sep 10, 2025
f091fcb
Add gsumfzsnfd to iset.mm
jkingdon Sep 10, 2025
06b6d2d
Add gsumsnd , gsumsnf , gsumsn to mmil.html
jkingdon Sep 10, 2025
215d997
add gsumpr to mmil.html
jkingdon Sep 10, 2025
6794ab6
Add mpocnfldadd to iset.mm
jkingdon Sep 11, 2025
18e8340
Add gsumfzfsum to iset.mm
jkingdon Sep 10, 2025
5f716ce
Add submmulg to iset.mm
jkingdon Sep 11, 2025
4557909
Add mpocnfldmul to iset.mm
jkingdon Sep 12, 2025
09b3242
Add cnfldui to iset.mm
jkingdon Sep 12, 2025
c4bffaf
Add expghmap to iset.mm
jkingdon Sep 11, 2025
50f2229
Add lgseisenlem4 to iset.mm
jkingdon Sep 11, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions iset-discouraged
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,7 @@
"ax-addf" is used by "addcncntop".
"ax-addf" is used by "addex".
"ax-addf" is used by "cnfldplusf".
"ax-addf" is used by "mpocnfldadd".
"ax-addrcl" is used by "readdcl".
"ax-arch" is used by "arch".
"ax-caucvg" is used by "caucvgre".
Expand All @@ -86,6 +87,7 @@
"ax-mulass" is used by "mulass".
"ax-mulcl" is used by "mulcl".
"ax-mulcom" is used by "mulcom".
"ax-mulf" is used by "mpocnfldmul".
"ax-mulf" is used by "mulcncntop".
"ax-mulf" is used by "mulex".
"ax-mulrcl" is used by "remulcl".
Expand Down Expand Up @@ -354,7 +356,7 @@ New usage of "ax-1re" is discouraged (1 uses).
New usage of "ax-addass" is discouraged (1 uses).
New usage of "ax-addcl" is discouraged (1 uses).
New usage of "ax-addcom" is discouraged (1 uses).
New usage of "ax-addf" is discouraged (3 uses).
New usage of "ax-addf" is discouraged (4 uses).
New usage of "ax-addrcl" is discouraged (1 uses).
New usage of "ax-arch" is discouraged (1 uses).
New usage of "ax-caucvg" is discouraged (1 uses).
Expand All @@ -370,7 +372,7 @@ New usage of "ax-io" is discouraged (1 uses).
New usage of "ax-mulass" is discouraged (1 uses).
New usage of "ax-mulcl" is discouraged (1 uses).
New usage of "ax-mulcom" is discouraged (1 uses).
New usage of "ax-mulf" is discouraged (2 uses).
New usage of "ax-mulf" is discouraged (3 uses).
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is it nessesary to use discouraged theorems here? Aren't there corresponding not discouraged theorems available?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The short answer is that the two choices are to use https://us.metamath.org/ileuni/cnfldmul.html (already in iset.mm) or add mpocnfldmul (as it is stated in set.mm). The most plausible way to prove mpocnfldmul in the short run is via ax-mulf. The cnfldmul approach wouldn't show up as an additional use of a discouraged theorem but it would actually entrench ax-mulf further.

I don't know how familiar you are with the ax-mulf background but in a nutshell:

There are also some dissenting voices:

I'm not really trying to get involved in something which is still being worked out in set.mm - I am just trying to follow current set.mm practice as readily as can be done without a large amount of effort.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK, if this is still in discussion in set.mm, we can take its current state over to iset.mm.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, that's pretty much the situation. Even if/when things settle down in set.mm, it is still work to bring it over to iset.mm (adjusting as needed for the differences between the two) - my philosophy for how to do that is "one step at a time".

New usage of "ax-mulrcl" is discouraged (1 uses).
New usage of "ax0id" is discouraged (0 uses).
New usage of "ax0lt1" is discouraged (0 uses).
Expand Down
Loading