English
If multiplication on a monoid is continuous, then multiplication on its units is continuous (with the induced topology).
Русский
Если умножение на моноиде непрерывно, то умножение на единицы моноида непрерывно (с индукционной топологией).
LaTeX
$$$\\text{ContinuousMul } M \\Rightarrow \\text{ContinuousMul } M^{\\times}$$$
Lean4
/-- If multiplication on a monoid is continuous, then multiplication on the units of the monoid,
with respect to the induced topology, is continuous.
Inversion is also continuous, but we register this in a later file, `Topology.Algebra.Group`,
because the predicate `ContinuousInv` has not yet been defined. -/
@[to_additive /-- If addition on an additive monoid is continuous, then addition on the additive
units of the monoid, with respect to the induced topology, is continuous.
Negation is also continuous, but we register this in a later file, `Topology.Algebra.Group`, because
the predicate `ContinuousNeg` has not yet been defined. -/
]
instance : ContinuousMul αˣ :=
isInducing_embedProduct.continuousMul (embedProduct α)
