vadd_vsub

Mathlib.Algebra.AddTorsor.Defs

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

← MathLib Explorer

English

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

Русский

Для любого g ∈ G и p1, p2 ∈ P верно (g +ᵥ p1) −ᵥ p2 = g + (p1 −ᵥ p2).

LaTeX

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

Lean4

/-- Adding a group element then subtracting the original point
produces that group element. -/
@[simp]
theorem vadd_vsub (g : G) (p : P) : (g +ᵥ p) -ᵥ p = g :=
  AddTorsor.vadd_vsub' g p

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

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

Разделы

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

Аффилиация

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