English
In a normed ring with a strictly multiplicative norm, right multiplication by a nonzero element a (i.e., b ↦ b a) also acts as a dilation, scaling distances by ‖a‖ on the right side.
Русский
В нормированном кольце с строго умножающейся нормой умножение справа на ненулевой элемент a (b ↦ b a) также является дилатацией, расстояния масштабируются на ‖a‖ справа.
LaTeX
$$$d(b\,a, c\,a) = \|a\| \, d(b,c) \\text{ for all } b,c\in A.$$$
Lean4
/-- Multiplication by a nonzero element `a` on the right, as a `Dilation` of a ring with a strictly
multiplicative norm. -/
@[simps!]
def mulRight (a : α) (ha : a ≠ 0) : α →ᵈ α where
toFun b := b * a
edist_eq' :=
⟨‖a‖₊, nnnorm_ne_zero_iff.2 ha, fun x y ↦ by simp [edist_nndist, nndist_eq_nnnorm, ← sub_mul, ← mul_comm (‖a‖₊)]⟩
