projective): weaken assumptions in lifting_property (#16750)

Commit

3 years ago

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`.

Author

antoinelab01

Parents

8818d823

mathlib 08bb56fb - feat(algebra/module/projective): weaken assumptions in lifting_property (#16750)

mathlib
08bb56fb - feat(algebra/module/projective): weaken assumptions in lifting_property (#16750)