mathlib

40ffaa5a - feat(linear_algebra/free_module): add module.free.resolution (#8231)

feat(linear_algebra/free_module): add module.free.resolution (#8231) Any module is a quotient of a free module. This is stated as surjectivity of `finsupp.total M M R id : (M →₀ R) →ₗ[R] M`.