We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 761725c commit e9c4b77Copy full SHA for e9c4b77
1 file changed
Mathlib/Topology/Algebra/Group/Units.lean
@@ -21,7 +21,7 @@ open Units
21
of the units of the monoid. -/
22
@[to_additive]
23
lemma Submonoid.isOpen_units {M : Type*} [TopologicalSpace M] [Monoid M]
24
- {U : Submonoid M} (hU : IsOpen (U : Set M)) : IsOpen (U.units : Set Mˣ) :=
+ {U : Submonoid M} (hU : IsOpen (U : Set M)) : IsOpen (U.units : Set Mˣ) :=
25
(hU.preimage Units.continuous_val).inter (hU.preimage Units.continuous_coe_inv)
26
27
/-- The monoid homeomorphism between the units of a product of topological monoids
0 commit comments