vadd_vsub_vadd_cancel_right

Mathlib.Algebra.AddTorsor.Defs

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

← MathLib Explorer

English

For v1,v2 ∈ G and p ∈ P, (v1 +ᵥ p) -ᵥ (v2 +ᵥ p) = v1 - v2.

Русский

Для v1,v2 ∈ G и p ∈ P: (v1 +ᵥ p) -ᵥ (v2 +ᵥ p) = v1 - v2.

LaTeX

$$$(v_1 +ᵥ p) -ᵥ (v_2 +ᵥ p) = v_1 - v_2$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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