eq_of_vsub_eq_zero

Mathlib.Algebra.AddTorsor.Defs

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

← MathLib Explorer

English

If p1 -ᵥ p2 = 0, then p1 = p2.

Русский

Если p1 -ᵥ p2 = 0, то p1 = p2.

LaTeX

$$$vsub(p_1,p_2) = 0_G \Rightarrow p_1 = p_2$$$

Lean4

/-- If subtracting two points produces 0, they are equal. -/
theorem eq_of_vsub_eq_zero {p₁ p₂ : P} (h : p₁ -ᵥ p₂ = (0 : G)) : p₁ = p₂ := by rw [← vsub_vadd p₁ p₂, h, zero_vadd]

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

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

Разделы

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

Аффилиация

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