symmetric monoidal (∞,1)-category of spectra
We see how this is equivalent to the classical definition of a basis as a linearly independent spanning set:
A basis for a free -module determines a unique generating set for of linearly independent elements of .
Fix a basis for over . Then let for each . Since is an isomorphism, each determines a unique element . Since every element of is of the form for , and since every element of can be written as a finite -linear combination of the , this proves that generates . To show linear independence, we again apply and its linearity. The result is immediate.