Metamath Proof Explorer


Syntax definition clsm

Description: Extend class notation with subgroup sum.

Ref Expression
Assertion clsm class LSSum