inversion_dist_center — Mathlib

English

Alternative formulation of the previous distance relation.

Русский

Альтернативная формулировка предыдущего соотношения расстояний.

LaTeX

$$$\text{(same as 117295 in different guise)}$$$

Lean4

@[simp]
theorem inversion_dist_center (c x : P) : inversion c (dist x c) x = x :=
  by
  rcases eq_or_ne x c with (rfl | hne)
  · apply inversion_self
  · rw [inversion, div_self, one_pow, one_smul, vsub_vadd]
    rwa [dist_ne_zero]

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