Commit 2022-10-03 05:43 08bb56fb
View on Github →feat(algebra/module/projective): weaken assumptions in lifting_property (#16750)
These add_comm_group structures are not necessary, nor is the universe restriction on M.
feat(algebra/module/projective): weaken assumptions in lifting_property (#16750)
These add_comm_group structures are not necessary, nor is the universe restriction on M.