uniformContinuousConstSMul_op — Mathlib

English

The action of a ring on itself by multiplication is uniformly continuous when the ring carries a compatible uniform structure.

Русский

Действие кольца на себя через умножение равномерно непрерывно при наличии совместимой униформной структуры.

LaTeX

$$$UniformContinuousConstSMul\; R\; R$$$

Lean4

/-- The action of `Semiring.toOppositeModule` is uniformly continuous. -/
instance uniformContinuousConstSMul_op [Ring R] [UniformSpace R] [IsUniformAddGroup R] [ContinuousMul R] :
    UniformContinuousConstSMul Rᵐᵒᵖ R :=
  uniformContinuousConstSMul_of_continuousConstSMul _ _

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