Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Extended real and complex numbers, real and complex projective lines
Argument, multiplication and inverse
carg
Next ⟩
df-bj-arg
Metamath Proof Explorer
Unicode
Structured
Syntax definition
carg
Description:
Syntax for the argument of a nonzero extended complex number.
Ref
Expression
Assertion
carg
class Arg