English
In the commutative case, with mul_comm, the same construction as SeminormedGroup.ofMulDist yields a SeminormedCommGroup structure.
Русский
В коммутативном случае, при наличии mul_comm, та же конструкция, что и SeminormedGroup.ofMulDist, задаёт SeminormedCommGroup.
LaTeX
$$$\text{SeminormedCommGroup.ofMulDist } h$ yields a SeminormedCommGroup with mul_comm := mul_comm.$$
Lean4
/-- Construct a seminormed group from a multiplication-invariant pseudodistance. -/
@[to_additive /-- Construct a seminormed group from a translation-invariant pseudodistance. -/
]
abbrev ofMulDist [Norm E] [CommGroup E] [PseudoMetricSpace E] (h₁ : ∀ x : E, ‖x‖ = dist x 1)
(h₂ : ∀ x y z : E, dist x y ≤ dist (x * z) (y * z)) : SeminormedCommGroup E :=
{ SeminormedGroup.ofMulDist h₁ h₂ with mul_comm := mul_comm }
-- See note [reducible non-instances]
