Database
BASIC ALGEBRAIC STRUCTURES
Division rings and fields
Definition and basic properties
drnggrpd
Next ⟩
drnggrp
Metamath Proof Explorer
Ascii
Unicode
Theorem
drnggrpd
Description:
A division ring is a group (deduction form).
(Contributed by
SN
, 16-May-2024)
Ref
Expression
Hypothesis
drngringd.1
⊢
φ
→
R
∈
DivRing
Assertion
drnggrpd
⊢
φ
→
R
∈
Grp
Proof
Step
Hyp
Ref
Expression
1
drngringd.1
⊢
φ
→
R
∈
DivRing
2
1
drngringd
⊢
φ
→
R
∈
Ring
3
2
ringgrpd
⊢
φ
→
R
∈
Grp