right_vsub_pointReflection

Mathlib.Algebra.AddTorsor.Basic

URI: https://scilib.ai/kg/mathlib#Equiv.right_vsub_pointReflection

English

For x, y ∈ P, y −ᵥ pointReflection x y = 2 · (y −ᵥ x).

Русский

Для x, y ∈ P верно y −ᵥ pointReflection x y = 2 · (y −ᵥ x).

LaTeX

$$$$ y -_{v} \text{pointReflection } x y = 2 \cdot (y -_{v} x) $$$$

Lean4

@[simp]
theorem right_vsub_pointReflection (x y : P) : y -ᵥ pointReflection x y = 2 • (y -ᵥ x) :=
  neg_injective <| by simp [← neg_nsmul]

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

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

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru