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
Unicode
Structured
Syntax definition
crefld
Description:
Extend class notation with the field of real numbers.
Ref
Expression
Assertion
crefld
class RRfld