Commit 2021-07-12 10:54 40ffaa5a

View on Github →

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.

Estimated changes

Modified src/algebra/module/projective.lean

Modified src/linear_algebra/finsupp.lean

added theorem finsupp.total_id_surjective

added theorem finsupp.total_range

added theorem finsupp.total_surjective

Modified src/linear_algebra/free_module.lean