Metamath Proof Explorer


Syntax definition crh

Description: Extend class notation with the ring homomorphisms.

Ref Expression
Assertion crh class RingHom