fix: add docstring for additive version of isOpen_units and fix deprecated syntax

Addresses review comment from plp127 about missing docstring for the additive version.
Also fixes the deprecated string syntax warning for to_additive attribute.

Author: kim-em

Mathlib/Topology/Algebra/Group/Units.lean

@@ -19,7 +19,8 @@ open Units
 
 /-- If a submonoid is open in a topological monoid, then its units form an open subset
 of the units of the monoid. -/
-@[to_additive]
+@[to_additive /-- If a subgroup of the additive units is open in a topological additive monoid,
+then its additive units form an open subset of the additive units of the monoid. -/]
 lemma Submonoid.isOpen_units {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)