Description: Define the identity polynomial. (Contributed by Mario Carneiro, 17-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | df-idp | ⊢ Xp = ( I ↾ ℂ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cidp | ⊢ Xp | |
1 | cid | ⊢ I | |
2 | cc | ⊢ ℂ | |
3 | 1 2 | cres | ⊢ ( I ↾ ℂ ) |
4 | 0 3 | wceq | ⊢ Xp = ( I ↾ ℂ ) |