Description: The finite free module is a power of the ring module. (Contributed by Stefan O'Rear, 1-Feb-2015)