Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-25 15:58 a617d0a6

View on Github →

feat(algebra/category/Module): R-mod has enough projectives (#7113) Another piece of @TwoFX's projective branch, lightly edited.

Estimated changes

Created src/algebra/category/Module/projective.lean

added theorem Module.projective_of_free

added theorem is_projective.iff_projective

Modified src/algebra/module/projective.lean

added theorem is_projective.of_lifting_property'

modified theorem is_projective.of_lifting_property