Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-19 09:07 15a64f53

View on Github →

feat(algebra/module/projective): add projective module (#6813) Definition and universal property of projective modules; free modules are projective.

Estimated changes

added theorem is_projective.of_free
added def is_projective