vsub_vadd

Mathlib.Algebra.AddTorsor.Defs

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

← MathLib Explorer

English

For all p1, p2 ∈ P, (p1 −ᵥ p2) +ᵥ p2 = p1.

Русский

Для любых p1, p2 ∈ P верно (p1 −ᵥ p2) +ᵥ p2 = p1.

LaTeX

$$$$ (p_1 -_{v} p_2) +_{v} p_2 = p_1 $$$$

Lean4

/-- Adding the result of subtracting from another point produces that
point. -/
@[simp]
theorem vsub_vadd (p₁ p₂ : P) : (p₁ -ᵥ p₂) +ᵥ p₂ = p₁ :=
  AddTorsor.vsub_vadd' p₁ p₂

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

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

Разделы

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

Аффилиация

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