Skip to content
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

Add CCfld to iset.mm #4678

Merged
merged 18 commits into from
Feb 28, 2025
Merged

Add CCfld to iset.mm #4678

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
8de10d2
copy plusgndxnn and basendxltplusgndx to iset.mm
jkingdon Feb 26, 2025
90aacb2
Copy more slot theorems from set.mm to iset.mm
jkingdon Feb 26, 2025
6dfba84
add grpstrndx to mmil.html
jkingdon Feb 26, 2025
da1c86c
add more scalar product slot theorems to iset.mm
jkingdon Feb 26, 2025
2e72b22
Add inner product slot theorems to iset.mm
jkingdon Feb 26, 2025
27a914b
Add le slot theorems to iset.mm
jkingdon Feb 26, 2025
b0a70f9
Add UnifSet slot theorems to iset.mm
jkingdon Feb 26, 2025
6a270d5
Trim iset.mm comments
jkingdon Feb 27, 2025
11d4ac0
Add strext to iset.mm
jkingdon Feb 26, 2025
048b0f1
Add CCfld to iset.mm
jkingdon Feb 22, 2025
8dea8ee
copy cnfldex from set.mm to iset.mm
jkingdon Feb 27, 2025
866e8d1
Add cnfldbas to iset.mm
jkingdon Feb 27, 2025
bd8d02b
copy addex and mulex from set.mm to iset.mm
jkingdon Feb 27, 2025
eb73b4b
add cnfldadd to iset.mm
jkingdon Feb 27, 2025
4980c57
Add cnfldmul to iset.mm
jkingdon Feb 27, 2025
517fc5d
Add cnfldcj to iset.mm
jkingdon Feb 27, 2025
dbd60ed
Update cnfld entries in mmil.html
jkingdon Feb 27, 2025
258cefd
Add more CCfld theorems to mmil.html
jkingdon Feb 27, 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
25 changes: 22 additions & 3 deletions iset-discouraged
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,7 @@
"ax-addcl" is used by "addcl".
"ax-addcom" is used by "addcom".
"ax-addf" is used by "addcncntop".
"ax-addf" is used by "addex".
"ax-addrcl" is used by "readdcl".
"ax-arch" is used by "arch".
"ax-caucvg" is used by "caucvgre".
Expand All @@ -79,6 +80,7 @@
"ax-mulcl" is used by "mulcl".
"ax-mulcom" is used by "mulcom".
"ax-mulf" is used by "mulcncntop".
"ax-mulf" is used by "mulex".
"ax-mulrcl" is used by "remulcl".
"ax16ALT" is used by "dvelimALT".
"ax16ALT" is used by "dvelimfv".
Expand Down Expand Up @@ -108,12 +110,18 @@
"basendx" is used by "2strstr1g".
"basendx" is used by "2strstrg".
"basendx" is used by "basendxltdsndx".
"basendx" is used by "basendxltplendx".
"basendx" is used by "basendxltplusgndx".
"basendx" is used by "basendxlttsetndx".
"basendx" is used by "basendxltunifndx".
"basendx" is used by "ipndxnbasendx".
"basendx" is used by "lmodstrd".
"basendx" is used by "rngstrg".
"basendx" is used by "scandxnbasendx".
"basendx" is used by "setsmsbasg".
"basendx" is used by "starvndxnbasendx".
"basendx" is used by "topgrpstrd".
"basendx" is used by "vscandxnbasendx".
"bj-axemptylem" is used by "bj-axempty".
"bj-axemptylem" is used by "bj-axempty2".
"cbv3" is used by "bdsetindis".
Expand All @@ -132,6 +140,11 @@
"csbco" is used by "zsumdc".
"df-div" is used by "divfnzn".
"df-div" is used by "divvalap".
"df-icnfld" is used by "cnfldadd".
"df-icnfld" is used by "cnfldbas".
"df-icnfld" is used by "cnfldcj".
"df-icnfld" is used by "cnfldmul".
"df-icnfld" is used by "cnfldstr".
"df-ilim" is used by "dflim2".
"df-inn" is used by "dfnn2".
"df-iom" is used by "dfom3".
Expand Down Expand Up @@ -288,6 +301,10 @@
"strnfvn" is used by "baseval".
"strnfvn" is used by "ndxarg".
"strnfvn" is used by "strsl0".
"unifndx" is used by "basendxltunifndx".
"unifndx" is used by "slotsdifunifndx".
"unifndx" is used by "unifndxnn".
"unifndx" is used by "unifndxntsetndx".
New usage of "0cnALT" is discouraged (0 uses).
New usage of "0reALT" is discouraged (0 uses).
New usage of "19.21h" is discouraged (3 uses).
Expand All @@ -310,7 +327,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 (1 uses).
New usage of "ax-addf" is discouraged (2 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 @@ -326,7 +343,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 (1 uses).
New usage of "ax-mulf" is discouraged (2 uses).
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 Expand Up @@ -367,7 +384,7 @@ New usage of "axpre-suploc" is discouraged (0 uses).
New usage of "axprecex" is discouraged (2 uses).
New usage of "axresscn" is discouraged (4 uses).
New usage of "axrnegex" is discouraged (0 uses).
New usage of "basendx" is discouraged (12 uses).
New usage of "basendx" is discouraged (18 uses).
New usage of "baseval" is discouraged (0 uses).
New usage of "bdcnulALT" is discouraged (0 uses).
New usage of "bdnthALT" is discouraged (0 uses).
Expand All @@ -392,6 +409,7 @@ New usage of "dcapnconstALT" is discouraged (0 uses).
New usage of "dcnnOLD" is discouraged (0 uses).
New usage of "demoivreALT" is discouraged (0 uses).
New usage of "df-div" is discouraged (2 uses).
New usage of "df-icnfld" is discouraged (5 uses).
New usage of "df-ilim" is discouraged (1 uses).
New usage of "df-inn" is discouraged (1 uses).
New usage of "df-iom" is discouraged (1 uses).
Expand Down Expand Up @@ -449,6 +467,7 @@ New usage of "stoic2b" is discouraged (0 uses).
New usage of "strcollnfALT" is discouraged (0 uses).
New usage of "strnfvn" is discouraged (3 uses).
New usage of "tfri1dALT" is discouraged (0 uses).
New usage of "unifndx" is discouraged (4 uses).
New usage of "uzind4ALT" is discouraged (0 uses).
New usage of "xpexgALT" is discouraged (0 uses).
Proof modification of "0cnALT" is discouraged (49 steps).
Expand Down
Loading