Skip to content

Commit

Permalink
AKS E and field hom injective (#4542)
Browse files Browse the repository at this point in the history 
* AKS E and field hom injective

* move 4 rhm theorems to main

* Change label and fix typo

* suggestion jkingdon

* typo
  • Loading branch information
@metakunt
metakunt authored Jan 9, 2025
1 parent 3dba285 commit ae7fe1b
Show file tree
Hide file tree
Showing 2 changed files with 236 additions and 77 deletions.
6 changes: 5 additions & 1 deletion changes-set.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,6 +92,10 @@ make a github issue.)

DONE:
Date Old New Notes
7-Jan-25 rhmdvdsr [same] Moved from TA's mathbox to main set.mm
7-Jan-25 rhmopp [same] Moved from TA's mathbox to main set.mm
7-Jan-25 elrhmunit [same] Moved from TA's mathbox to main set.mm
7-Jan-25 rhmunitinv [same] Moved from TA's mathbox to main set.mm
7-Jan-25 ringi ringdilem
5-Jan-25 nfrexd nfrexdw consistent with nfraldw
5-Jan-25 nfrex nfrexw consistent with nfralw
Expand Down Expand Up @@ -281,7 +285,7 @@ Date Old New Notes
26-Jun-24 rp-imass resssxp moved from RP's mathbox to main set.mm
26-Jun-24 sscon34b [same] moved from RP's mathbox to main set.mm
26-Jun-24 rcompleq [same] moved from RP's mathbox to main set.mm
26-Jun-24 funresd [same] moved from GS's mathbox to main set.mm
26-Jun-24 funresd [same] moved from GS's mathbox to main set.mmisCyclic_of_subgroup_isDomain
26-Jun-24 cmnmndd [same] moved from SN's mathbox to main set.mm
26-Jun-24 syl6req eqtr2di compare to eqtr2i or eqtr2d
16-Jun-24 syl6eqr eqtr4di compare to eqtr4i or eqtr4d
Expand Down
Loading

1 comment on commit ae7fe1b

@langgerard
Copy link

Choose a reason for hiding this comment

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

It seems that your theorem fldhmf1 does not use commutativity, and so is valid for division algebras.
Maybe you could change the name and transfer the theorem in the main part of set.mm

Please sign in to comment.