Metamath Proof Explorer


Syntax definition cmzpcl

Description: Extend class notation to include pre-polynomial rings.

Ref Expression
Assertion cmzpcl class mzPolyCld