vsub_sub_vsub_cancel_right

Mathlib.Algebra.AddTorsor.Defs

URI: https://scilib.ai/kg/mathlib#vsub_sub_vsub_cancel_right

← MathLib Explorer

English

Cancellation on the right: p1 -ᵥ p3 - (p2 -ᵥ p3) = p1 -ᵥ p2.

Русский

Правая отмена: p1 -ᵥ p3 - (p2 -ᵥ p3) = p1 -ᵥ p2.

LaTeX

$$$p_1 -ᵥ p_3 - (p_2 -ᵥ p_3) = p_1 -ᵥ p_2$$$

Lean4

/-- Cancellation subtracting the results of two subtractions. -/
@[simp]
theorem vsub_sub_vsub_cancel_right (p₁ p₂ p₃ : P) : p₁ -ᵥ p₃ - (p₂ -ᵥ p₃) = p₁ -ᵥ p₂ := by
  rw [← vsub_vadd_eq_vsub_sub, vsub_vadd]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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