fst_vsub

Mathlib.Algebra.AddTorsor.Basic

URI: https://scilib.ai/kg/mathlib#Prod.fst_vsub

English

For p1 = (a, b) and p2 = (c, d) in P × P', the first projection of p1 −ᵥ p2 is a −ᵥ c.

Русский

Для p1 = (a,b) и p2 = (c,d) из P × P' первая компонента p1 −ᵥ p2 равна a −ᵥ c.

LaTeX

$$$$(p_1 -ᵥ p_2).1 = p_1.1 -ᵥ p_2.1$$$$

Lean4

@[simp]
theorem fst_vsub (p₁ p₂ : P × P') : (p₁ -ᵥ p₂ : G × G').1 = p₁.1 -ᵥ p₂.1 :=
  rfl

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

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

Разделы

Аффилиация

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