English
Let A be a ring with a strictly multiplicative norm. For any nonzero a in A, the map L_a: A → A given by L_a(b) = a b is a dilation of the space, with the distortion factor equal to the norm of a. In particular, distance scales by ‖a‖ when both arguments are multiplied on the left by a.
Русский
Пусть A — кольцо с строго умножающейся нормой. Для любого ненулевого a ∈ A отображение L_a: A → A, L_a(b) = a b, является дилатацией пространства, коэффициент искажения равен ‖a‖. В частности, расстояние при умножении слева на a масштабируется на ‖a‖.
LaTeX
$$$d(a\,b, a\,c) = \|a\| \, d(b,c) \\text{ for all } b,c\in A.$$$
Lean4
/-- Multiplication by a nonzero element `a` on the left, as a `Dilation` of a ring with a strictly
multiplicative norm. -/
@[simps!]
def mulLeft (a : α) (ha : a ≠ 0) : α →ᵈ α where
toFun b := a * b
edist_eq' := ⟨‖a‖₊, nnnorm_ne_zero_iff.2 ha, fun x y ↦ by simp [edist_nndist, nndist_eq_nnnorm, ← mul_sub]⟩
