units_continuousConstSMul — Mathlib

English

The conjugation action of units on a monoid M is continuous; equivalently, the map (u,a) ↦ u a u⁻¹ from Units(M) × M to M is continuous.

Русский

Действие конъюгации единиц на полугруппу M непрерывно; эквивалентно непрерывности отображения (u,a) ↦ u a u⁻¹.

LaTeX

$$$\text{ContinuousConstSMul}(\text{ConjAct}(\mathrm{Units}(M)), M).$$$

Lean4

instance units_continuousConstSMul {M} [Monoid M] [TopologicalSpace M] [ContinuousMul M] :
    ContinuousConstSMul (ConjAct Mˣ) M :=
  ⟨fun _ => (continuous_const.mul continuous_id).mul continuous_const⟩

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