Metamath Proof Explorer


Syntax definition clininds

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

Ref Expression
Assertion clininds class linIndS