Definition df-nmcv

Description: Define the norm function in a normed complex vector space. (Contributed by NM, 25-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Assertion	df-nmcv	⊢ normCV = 2nd

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnmcv	⊢ normCV
1		c2nd	⊢ 2nd
2	0 1	wceq	⊢ normCV = 2nd