instTopologicalSpaceUnits — Mathlib

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

Похожие утверждения