Solution (source code)

= Solution

A subset $E\subseteq M$ is a <basis of a module> if every $m\in M$ has a unique expression
$$
\boxed{m=\sum_{e\in E}r_ee,\qquad r_e\in R,\qquad r_e=0\text{ for all but finitely many }e}.
$$
Uniqueness concerns the entire family of coefficients, including the zero coefficients. Equivalently, $E$ generates $M$ and is <linearly independent in a module>: every finite relation $\sum_{e\in H}r_ee=0$, with $H\subseteq E$, has all $r_e=0$.

A <module> is a <free module> if it has a <basis of a module>. An infinite <basis of a module> still uses only finite sums in each expression; arbitrary infinite sums are not part of the <module> operations.