snd_vadd

Mathlib.Algebra.AddTorsor.Basic

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

English

For v = (v1, v2) ∈ G × G' and p = (p1, p2) ∈ P × P', the second coordinate of v +ᵥ p is v2 +ᵥ p2.

Русский

Для v = (v1, v2) ∈ G × G' и p = (p1, p2) ∈ P × P' вторая координата v +ᵥ p равна v2 +ᵥ p2.

LaTeX

$$$$(v +ᵥ p).2 = v.2 +ᵥ p.2$$$$

Lean4

@[simp]
theorem snd_vadd (v : G × G') (p : P × P') : (v +ᵥ p).2 = v.2 +ᵥ p.2 :=
  rfl

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

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

Разделы

Аффилиация

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