Metamath Proof Explorer


Syntax definition crs

Description: Extend class notation with the ring isomorphisms.

Ref Expression
Assertion crs class RingIso