English
The units of a monoid M are equipped with the topology induced by embedding into M × M via u ↦ (u, u^{-1}).
Русский
Единицы моноида M наделяются топологией, индуцированной вложением в M × M через m ↦ (m, m^{-1}).
LaTeX
$$$$ \operatorname{TopologicalSpace}(M^{\times}) = \operatorname{TopologicalSpace.induced}(\mathrm{embedProduct}(M), \operatorname{TopologicalSpace}(M)) $$$$
Lean4
/-- The units of a monoid are equipped with a topology, via the embedding into `M × M`. -/
@[to_additive /-- The additive units of a monoid are equipped with a topology, via the embedding into `M × M`. -/
]
instance instTopologicalSpaceUnits : TopologicalSpace Mˣ :=
TopologicalSpace.induced (embedProduct M) inferInstance