Mathlib v3 is deprecated. Go to Mathlib v4

Structure category_theory.glue_data

Modification history

2021-12-18 10:22
src/category_theory/glue_data.lean
feat(category_theory): Glue data (#10436)
Added category_theory.glue_dataView on Github →