Metamath Proof Explorer


Syntax definition cidp

Description: Extend class notation to include the identity polynomial.

Ref Expression
Assertion cidp class Xp