Def Born

Modification history

2025-02-05 23:58

Mathlib/Topology/Category/Born.lean

refactor(Topology/Category): clean up remaining uses of `HasForget` (#21458) …

Deleted Born View on Github →

2023-03-18 15:20

Mathlib/Topology/Category/Born.lean

feat: port Topology.Category.Born (#2973)

Added Born View on Github →