Def. finSupp, example for linearly dependent sets
Def. finSupp, example for linearly dependent sets

* Definition of the predicate "finitely supported function" (` finSupp `)
* Additional theorems for the ring of integers
* Additional theorems for the `ZZ `-module ` ZZ X. ZZ
* Example for a linearly dependent set in a module (not being a vector space) in which none of the elements can be represented as lin. combination of the other(s).

metamath/set.mm,metamath/set.mm,metamath/set.mm