Metamath Proof Explorer


Syntax definition cdvr

Description: Extend class notation with ring division.

Ref Expression
Assertion cdvr class / r