Definition df-0p

Description: Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Assertion	df-0p	⊢ 0𝑝 = ( ℂ × { 0 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c0p	⊢ 0𝑝
1		cc	⊢ ℂ
2		cc0	⊢ 0
3	2	csn	⊢ { 0 }
4	1 3	cxp	⊢ ( ℂ × { 0 } )
5	0 4	wceq	⊢ 0𝑝 = ( ℂ × { 0 } )