vsub_self

Mathlib.Algebra.AddTorsor.Defs

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

← MathLib Explorer

English

For every point p in P, the vector from p to p is the zero element of G.

Русский

Для любого p ∈ P вектор от p к p равен нулю в G.

LaTeX

$$$\forall p \in P:\ vsub(p,p) = 0_G$$$

Lean4

/-- Subtracting a point from itself produces 0. -/
@[simp]
theorem vsub_self (p : P) : p -ᵥ p = (0 : G) := by rw [← zero_add (p -ᵥ p), ← vadd_vsub_assoc, vadd_vsub]

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

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

Разделы

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

Аффилиация

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