Structure TopCat.GlueData

Modification history

2024-12-02 04:16

Mathlib/Topology/Gluing.lean

chore: bump toolchain to v4.15.0-rc1, and merge bump/v4.15.0 adaptations branch (#19675)

Modified TopCat.GlueData View on Github →

2023-06-14 11:40

Mathlib/Topology/Gluing.lean

feat: port Topology.Gluing (#3987)

Added TopCat.GlueData View on Github →