Database
BASIC ALGEBRAIC STRUCTURES
Division rings and fields
Definition and basic properties
fldcrngd
Next ⟩
isdrng2
Metamath Proof Explorer
Ascii
Unicode
Theorem
fldcrngd
Description:
A field is a commutative ring.
(Contributed by
SN
, 23-Nov-2024)
Ref
Expression
Hypothesis
fldcrngd.1
⊢
φ
→
R
∈
Field
Assertion
fldcrngd
⊢
φ
→
R
∈
CRing
Proof
Step
Hyp
Ref
Expression
1
fldcrngd.1
⊢
φ
→
R
∈
Field
2
isfld
⊢
R
∈
Field
↔
R
∈
DivRing
∧
R
∈
CRing
3
2
simprbi
⊢
R
∈
Field
→
R
∈
CRing
4
1
3
syl
⊢
φ
→
R
∈
CRing