vsub_add_vsub_cancel

Mathlib.Algebra.AddTorsor.Defs

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

← MathLib Explorer

English

Cancellation: p1 -ᵥ p2 + (p2 -ᵥ p3) = p1 -ᵥ p3.

Русский

Отмена: p1 -ᵥ p2 + (p2 -ᵥ p3) = p1 -ᵥ p3.

LaTeX

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

Lean4

/-- Cancellation adding the results of two subtractions. -/
@[simp]
theorem vsub_add_vsub_cancel (p₁ p₂ p₃ : P) : p₁ -ᵥ p₂ + (p₂ -ᵥ p₃) = p₁ -ᵥ p₃ :=
  by
  apply vadd_right_cancel p₃
  rw [add_vadd, vsub_vadd, vsub_vadd, vsub_vadd]

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

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

Разделы

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

Аффилиация

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