Skip to content

Commit

Permalink
Subfields generated by a set (#4553)
Browse files Browse the repository at this point in the history
* Subfields generated by a set

* Use sub-division-rings in the definition of generated subfields

* therefore > hence

* Shortened and renamed ~ recrng

* Update changes-set.txt

* Moved `fldsdrgfld` to main, comment updated.

* Rewrap

* fldcrng > fldcrngo

* Link to ~ fldsdrgfld in ~ df-sdrg

* Regen discouraged

* Editorial changes, and one shortening.

* Rewrap

* Update definition of sub-division-rings
  • Loading branch information
tirix authored Jan 14, 2025
1 parent 109857e commit 389a55a
Show file tree
Hide file tree
Showing 3 changed files with 180 additions and 59 deletions.
5 changes: 5 additions & 0 deletions changes-set.txt
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,8 @@ make a github issue.)

DONE:
Date Old New Notes
11-Jan-25 fldcrng fldcrngo
11-Jan-25 recrng resrng
11-Jan-25 --- --- Moved surreal ordering theorems from
SF's mathbox to main set.mm
11-Jan-25 --- --- Moved ordinal sequence theorems from
Expand All @@ -95,6 +97,9 @@ Date Old New Notes
11-Jan-25 3orel13 [same] Moved from SF's mathbox to main set.mm
11-Jan-25 3pm3.2ni [same] Moved from SF's mathbox to main set.mm
10-Jan-25 syl5bi biimtrid
10-Jan-25 fldcrngd [same] Moved from SN's mathbox to main set.mm
10-Jan-25 drngringd [same] Moved from SN's mathbox to main set.mm
10-Jan-25 drnggrpd [same] Moved from SN's mathbox to main set.mm
9-Jan-25 fvresval [same] Moved from SF's mathbox to main set.mm
9-Jan-25 brtp [same] Moved from SF's mathbox to main set.mm
9-Jan-25 --- --- Moved initial surreal definitions from
Expand Down
4 changes: 2 additions & 2 deletions discouraged
Original file line number Diff line number Diff line change
Expand Up @@ -4783,7 +4783,7 @@
"df-erq" is used by "nqerid".
"df-erq" is used by "nqerrel".
"df-exid" is used by "isexid".
"df-fld" is used by "fldcrng".
"df-fld" is used by "fldcrngo".
"df-fld" is used by "flddivrng".
"df-fld" is used by "isfld2".
"df-gcdOLD" is used by "ee7.2aOLD".
Expand Down Expand Up @@ -5563,7 +5563,7 @@
"drnfc1" is used by "nfcvb".
"drnfc1" is used by "nfriotad".
"drngoi" is used by "dvrunz".
"drngoi" is used by "fldcrng".
"drngoi" is used by "fldcrngo".
"drsb1" is used by "iotaeq".
"drsb1" is used by "sb2ae".
"drsb1" is used by "sbco3".
Expand Down
Loading

0 comments on commit 389a55a

Please sign in to comment.