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