Metamath Proof Explorer


Syntax definition clindeps

Description: Extend class notation with the relation between a module and its linearly dependent subsets.

Ref Expression
Assertion clindeps class linDepS