Uniformly continuous scalar actions on rings with an absolute value #
The algebra action of a commutative semiring on WithAbs v is uniformly continuous for every
fixed scalar. This lets the scalar action extend to the completion without requiring the scalar
semiring to be a ring.
@[instance 100]
instance
WithAbs.uniformContinuousConstSMul
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[Ring A]
[Algebra R A]
(v : AbsoluteValue A ℝ)
:
The algebra action on a ring with an absolute value is uniformly continuous in its argument.