Database
REAL AND COMPLEX NUMBERS
Construction and axiomatization of real and complex numbers
Dedekind-cut construction of real and complex numbers
caddc

Next ⟩ cltrr

Metamath Proof Explorer

Ascii
Unicode

Syntax definition caddc

Description: Addition on complex numbers.

		Ref	Expression
	Assertion	caddc	$class +$