Description: A division ring is a group (closed form). (Contributed by NM, 8-Sep-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | drnggrp | |- ( R e. DivRing -> R e. Grp ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | |- ( R e. DivRing -> R e. DivRing ) |
|
2 | 1 | drnggrpd | |- ( R e. DivRing -> R e. Grp ) |