Mathlib v3 is deprecated. Go to Mathlib v4

Def category_theory.glue_data.map_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_data.map_glue_dataView on Github →