Metamath Proof Explorer


Syntax definition crgspn

Description: Extend class notation with span of a set of elements over a ring.

Ref Expression
Assertion crgspn class RingSpan