Database
BASIC ALGEBRAIC STRUCTURES
Rings
Definition and basic properties of unital rings
crnggrpd
Next ⟩
mgpf
Metamath Proof Explorer
Ascii
Unicode
Theorem
crnggrpd
Description:
A commutative ring is a group.
(Contributed by
SN
, 16-May-2024)
Ref
Expression
Hypothesis
crngringd.1
⊢
φ
→
R
∈
CRing
Assertion
crnggrpd
⊢
φ
→
R
∈
Grp
Proof
Step
Hyp
Ref
Expression
1
crngringd.1
⊢
φ
→
R
∈
CRing
2
1
crngringd
⊢
φ
→
R
∈
Ring
3
2
ringgrpd
⊢
φ
→
R
∈
Grp