Metamath Proof Explorer


Syntax definition cdenom

Description: Extend class notation to include canonical denominator function.

Ref Expression
Assertion cdenom class denom