vadd_vsub_vadd_cancel_left

Mathlib.Algebra.AddTorsor.Basic

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

← MathLib Explorer

English

For any v ∈ G and p1, p2 ∈ P, (v +ᵥ p1) −ᵥ (v +ᵥ p2) = p1 −ᵥ p2.

Русский

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

LaTeX

$$$ (v +ᵥ p_1) -ᵥ (v +ᵥ p_2) = p_1 -ᵥ p_2 $$$

Lean4

@[simp]
theorem vadd_vsub_vadd_cancel_left (v : G) (p₁ p₂ : P) : (v +ᵥ p₁) -ᵥ (v +ᵥ p₂) = p₁ -ᵥ p₂ := by
  rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub_cancel_left]

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

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

Разделы

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

Аффилиация

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