Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_projective.iff_projective

Modification history

2021-05-25 15:58
src/algebra/category/Module/projective.lean
feat(algebra/category/Module): R-mod has enough projectives (#7113) …
Added is_projective.iff_projectiveView on Github →