Commit 2025-09-30 21:50 bb6ed240

View on Github →

feat: Units.{continuous_map,isOpenMap_map} (#29780)

Estimated changes

Modified Mathlib/Topology/Algebra/Constructions.lean

added theorem Units.continuous_map

added theorem Units.isOpenMap_map