to_isIsometricSMul_left — Mathlib

English

For every element a in the normed group, left multiplication by a is an isometry of the group.

Русский

Для каждого элемента a в нормированной группе левое умножение на a является изометрией группы.

LaTeX

$$$\forall a,\; \text{Isometry}(x \mapsto a \cdot x).$$$

Lean4

@[to_additive]
instance to_isIsometricSMul_left : IsIsometricSMul E E :=
  ⟨fun a => Isometry.of_dist_eq fun b c => by simp [dist_eq_norm_div]⟩

Похожие утверждения