fst_vadd

Mathlib.Algebra.AddTorsor.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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