mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

properties of (sub)modules

Open jcommelin opened this issue 5 years ago • 1 comments

  • [x] finite
  • [x] finitely generated (done for submodules, we might want a wrapper to make life easier when working with a full module) (#4634)
  • [ ] finitely presentable
  • [x] flat
  • [x] projective
  • [x] injective #12895

Feel free to add more. See also #4013.

jcommelin avatar Sep 03 '20 04:09 jcommelin