prod_fst

Mathlib.Data.TwoPointing

URI: https://scilib.ai/kg/mathlib#TwoPointing.prod_fst

English

The first component of the product two-pointing equals the pair of first components: (p.prod q).fst = (p.fst, q.fst).

Русский

Первая компонента произведения указателей равна паре первых компонентов: (p.prod q).fst = (p.fst, q.fst).

LaTeX

$$$(p.prod q).fst = (p.fst, q.fst)$$

Lean4

@[simp]
theorem prod_fst : (p.prod q).fst = (p.fst, q.fst) :=
  rfl

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

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

Разделы

Аффилиация

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