dist_self_div_right — Mathlib

English

There is a structure making left multiplication by any a an isometry of the group, i.e., dist(a x, a y) = dist(x, y) for all x,y.

Русский

Существует структура, делающая левое умножение на фиксированное a изометрией: ∀ x,y, dist(a x, a y) = dist(x,y).

LaTeX

$$$\forall a, \forall x,y,\ dist(a x, a y) = dist(x,y).$$$

Lean4

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

theorem dist_self_div_right (a b : E) : dist a (a / b) = ‖b‖ := by rw [div_eq_mul_inv, dist_self_mul_right, norm_inv']

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