snd_vsub

Mathlib.Algebra.AddTorsor.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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