Mathlib v3 is deprecated. Go to Mathlib v4

Theorem Module.projective_of_free

Modification history

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