dist_self_div_left — Mathlib

English

There is an isometric left action of E on itself by multiplication: each map x ↦ a x is an isometry.

Русский

Существует изометрическое левое действие E на себе через умножение: каждому a сопоставлена изометрия x ↦ a x.

LaTeX

$$$\text{IsIsometricSMul}(E,E) \text{ holds, i.e. } \forall a,x,y,\ \mathrm{dist}(a x, a y) = \mathrm{dist}(x,y).$$$

Lean4

@[to_additive (attr := simp 1001)] -- Increase priority because `simp` can prove this

theorem dist_self_div_left (a b : E) : dist (a / b) a = ‖b‖ := by rw [dist_comm, dist_self_div_right]

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