Database
BASIC ALGEBRAIC STRUCTURES
The complex numbers as an algebraic extensible structure
The ordered field of real numbers
crefld
Next ⟩
df-refld
Metamath Proof Explorer
Ascii
Structured
Syntax definition
crefld
Description:
Extend class notation with the field of real numbers.
Ref
Expression
Assertion
crefld
class
ℝ
fld