vadd_vsub_eq_sub_vsub

Mathlib.Algebra.AddTorsor.Defs

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

English

For g ∈ G and p,q ∈ P, (g +ᵥ p) -ᵥ q = g - (q -ᵥ p).

Русский

Для любого g ∈ G и p,q ∈ P выполняется (g +ᵥ p) -ᵥ q = g - (q -ᵥ p).

LaTeX

$$$(g +ᵥ p) -ᵥ q = g - (q -ᵥ p)$$$

Lean4

theorem vadd_vsub_eq_sub_vsub (g : G) (p q : P) : (g +ᵥ p) -ᵥ q = g - (q -ᵥ p) := by
  rw [vadd_vsub_assoc, sub_eq_add_neg, neg_vsub_eq_vsub_rev]

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

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

Разделы

Аффилиация

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