Commit 2024-12-16 13:15 0a6144da

View on Github →

feat(Topology): Introduce HomeomorphClass (#18689) Introduce HomeomorphClass

Estimated changes

Modified Mathlib/Topology/Algebra/Module/Basic.lean

Modified Mathlib/Topology/Homeomorph.lean

added theorem HomeomorphClass.coe_coe

added def HomeomorphClass.toHomeomorph

added theorem HomeomorphClass.toHomeomorph_injective