Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-22 15:37 dc5a3db9

View on Github →

feat(algebra/category): Forgetful functors preserve filtered colimits (#9101) Shows that forgetful functors of various algebraic categories preserve filtered colimits.

Estimated changes