Basic tensor proof entry point.

The submodules group algebraic, folding, bound, and linear-algebra facts about dependent tensors so other proof developments can import a coherent tensor toolkit.