Metamath Proof Explorer


Syntax definition cur

Description: Extend class notation with ring unit.

Ref Expression
Assertion cur class 1r