English
From a multiplication-invariant distance with ∥x∥ = dist(x,1) and left-invariance dist(x,y) ≤ dist(x z,y z), one obtains a NormedGroup structure on E with dist(x,y) = ∥x y^{-1}∥.
Русский
Из расстояния с инвариантностью умножения и условий ∥x∥ = dist(x,1) и dist(x,y) ≤ dist(x z,y z) получается структура NormedGroup на E с dist(x,y)=∥x y^{-1}∥.
LaTeX
$$$\text{If } ‖x‖ = dist(x,1) \text{ and } dist(x,y) ≤ dist(xz,yz),\; dist(x,y)=‖x y^{-1}‖$ defines a NormedGroup.$$
Lean4
/-- Construct a normed group from a multiplication-invariant distance. -/
@[to_additive /-- Construct a normed group from a translation-invariant distance. -/
]
abbrev ofMulDist [Norm E] [Group E] [MetricSpace E] (h₁ : ∀ x : E, ‖x‖ = dist x 1)
(h₂ : ∀ x y z : E, dist x y ≤ dist (x * z) (y * z)) : NormedGroup E :=
{ SeminormedGroup.ofMulDist h₁ h₂ with eq_of_dist_eq_zero := eq_of_dist_eq_zero }
-- See note [reducible non-instances]
