over): granularity in forget preserving colimits (#2941)

Commit

6 years ago

chore(category_theory/limits/over): granularity in forget preserving colimits (#2941) a bit more granularity for instances about forget preserving colimits

Author

b-mehta

Parents

97265f9c

mathlib3 494b43ef - chore(category_theory/limits/over): granularity in forget preserving colimits (#2941)

mathlib3
494b43ef - chore(category_theory/limits/over): granularity in forget preserving colimits (#2941)