Commit 2025-08-12 11:46 5debf979

View on Github →

feat(Topology/Algebra): Homeomorph version of unitsEquivNeZero (#25044) also add Topology.IsEmbedding.homeomorphImage: a set is homeomorphic to its image under any embedding.

Estimated changes

Modified Mathlib/Topology/Algebra/GroupWithZero.lean

modified theorem Units.isEmbedding_val₀

Modified Mathlib/Topology/Homeomorph/Lemmas.lean