mathlib

15a64f53 - feat(algebra/module/projective): add projective module (#6813)

feat(algebra/module/projective): add projective module (#6813) Definition and universal property of projective modules; free modules are projective. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>