dist_div_eq_dist_mul_right — Mathlib

English

Symmetrically, the distance between a and b/c equals the distance between a⋅c and b.

Русский

Симметрично, расстояние между a и b/c равно расстоянию между a⋅c и b.

LaTeX

$$$\\operatorname{dist}(a, \\tfrac{b}{c}) = \\operatorname{dist}(a\\cdot c, b)$$$

Lean4

@[to_additive (attr := simp)]
theorem dist_div_eq_dist_mul_right (a b c : E) : dist a (b / c) = dist (a * c) b := by
  rw [← dist_mul_right _ _ c, div_mul_cancel]

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