Metamath Proof Explorer


Syntax definition cmzp

Description: Extend class notation to include polynomial rings.

Ref Expression
Assertion cmzp class mzPoly