feat(Topology/Algebra/Group/Units): add topological properties of units

Add lemmas about units in topological monoids:
- `Submonoid.units_isOpen`: units of open submonoids are open
- `ContinuousMulEquiv.piUnits`: homeomorphism between units of product and product of units

Ported from the FLT project.

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>

Author: kim-em

Mathlib.lean

@@ -6296,6 +6296,7 @@ import Mathlib.Topology.Algebra.Group.Pointwise
 import Mathlib.Topology.Algebra.Group.Quotient
 import Mathlib.Topology.Algebra.Group.SubmonoidClosure
 import Mathlib.Topology.Algebra.Group.TopologicalAbelianization
+import Mathlib.Topology.Algebra.Group.Units
 import Mathlib.Topology.Algebra.GroupCompletion
 import Mathlib.Topology.Algebra.GroupWithZero
 import Mathlib.Topology.Algebra.Indicator

Mathlib/Topology/Algebra/Group/Units.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2025 Imperial College London. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Imperial College London FLT Project Contributors
+-/
+import Mathlib.Algebra.Group.Pi.Units
+import Mathlib.Algebra.Group.Submonoid.Units
+import Mathlib.Topology.Algebra.Constructions
+import Mathlib.Topology.Algebra.ContinuousMonoidHom
+import Mathlib.Topology.Algebra.Group.Basic
+
+/-!
+# Topological properties of units
+
+This file contains lemmas about the topology of units in topological monoids,
+including results about submonoid units and units of product spaces.
+-/
+
+open Units
+
+/-- If a submonoid is open in a topological monoid, then its units form an open subset
+of the units of the monoid. -/
+lemma Submonoid.units_isOpen {M : Type*} [TopologicalSpace M] [Monoid M]
+  {U : Submonoid M} (hU : IsOpen (U : Set M)) : IsOpen (U.units : Set Mˣ) :=
+  (hU.preimage Units.continuous_val).inter (hU.preimage Units.continuous_coe_inv)
+
+/-- The monoid homeomorphism between the units of a product of topological monoids
+and the product of the units of the monoids. -/
+def ContinuousMulEquiv.piUnits {ι : Type*}
+    {M : ι → Type*} [(i : ι) → Monoid (M i)] [(i : ι) → TopologicalSpace (M i)] :
+    (Π i, M i)ˣ ≃ₜ* Π i, (M i)ˣ where
+  __ := MulEquiv.piUnits
+  continuous_toFun := by
+    simp only [MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe]
+    refine continuous_pi (fun i => ?_)
+    refine Units.continuous_iff.mpr ⟨?_, ?_⟩
+    · simp only [Function.comp_def, MulEquiv.val_piUnits_apply]
+      exact (continuous_apply i).comp' Units.continuous_val
+    · simp only [MulEquiv.val_inv_piUnits_apply, Units.inv_eq_val_inv]
+      exact (continuous_apply i).comp' Units.continuous_coe_inv
+  continuous_invFun := by
+    simp only [MulEquiv.toEquiv_eq_coe, Equiv.invFun_as_coe, MulEquiv.coe_toEquiv_symm]
+    refine Units.continuous_iff.mpr ⟨?_, ?_⟩
+    · refine continuous_pi (fun i => ?_)
+      simp only [Function.comp_def, MulEquiv.val_piUnits_symm_apply]
+      exact Units.continuous_val.comp' (continuous_apply i)
+    · refine continuous_pi (fun i => ?_)
+      simp only [MulEquiv.val_inv_piUnits_symm_apply, Units.inv_eq_val_inv]
+      exact Units.continuous_coe_inv.comp' (continuous_apply i)