mathlib

efa6877b - feat(algebra/category/Module): the free/forgetful adjunction for R-modules (#6168)

feat(algebra/category/Module): the free/forgetful adjunction for R-modules (#6168) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>