Free modules #
Finsupp.total_id_surjective to prove that any module is the quotient of a free module.
Main definition #
Module.Free R M: the class of free
There is no hope of computing this, but we add the instance anyway to avoid fumbling with
open scoped Classical.
The universal property of free modules: giving a function
(ChooseBasisIndex R M) → N, for
R-module, is the same as giving an
M →ₗ[R] N.
This definition is parameterized over an extra
SMulCommClass R S M' holds.
R is commutative, you can set
S := R; if
R is not commutative,
you can recover an
AddEquiv by setting
S := ℕ.
See library note [bundled maps over different rings].