Metamath Proof Explorer


Syntax definition cidlsrg

Description: Extend class notation with the semiring of ideals of a ring.

Ref Expression
Assertion cidlsrg
class IDLsrg