The category of
R-modules has enough projectives. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
The categorical notion of projective object agrees with the explicit module-theoretic notion.
Modules that have a basis are projective.
The category of modules has enough projectives, since every module is a quotient of a free