Commit 2024-08-16 15:12 55e1bed5

View on Github →

refactor(Topology/Maps): use structure for QuotientMap (#15887)

Estimated changes

Modified Mathlib/Topology/Defs/Induced.lean

added structure QuotientMap

deleted def QuotientMap

Modified Mathlib/Topology/Maps/Basic.lean