vsub_eq_zero_iff_eq

Mathlib.Algebra.AddTorsor.Defs

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

← MathLib Explorer

English

For all p1,p2 in P, p1 -ᵥ p2 = 0 iff p1 = p2.

Русский

Для любых p1,p2 в P верно: p1 -ᵥ p2 = 0 тогда и только тогда, когда p1 = p2.

LaTeX

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

Lean4

/-- Subtracting two points produces 0 if and only if they are
equal. -/
@[simp]
theorem vsub_eq_zero_iff_eq {p₁ p₂ : P} : p₁ -ᵥ p₂ = (0 : G) ↔ p₁ = p₂ :=
  Iff.intro eq_of_vsub_eq_zero fun h => h ▸ vsub_self _

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

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

Разделы

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

Аффилиация

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