prod_map_id

Mathlib.Data.TypeVec

URI: https://scilib.ai/kg/mathlib#TypeVec.prod_map_id

English

Mapping identities on each component yields the identity on the product.

Русский

отображение идентичностей на компонентах даёт идентичность на произведении.

LaTeX

$$\operatorname{prod.map} \operatorname{id} \operatorname{id} = \operatorname{id}$$

Lean4

@[simp]
theorem prod_map_id {α β : TypeVec n} : (@TypeVec.id _ α ⊗' @TypeVec.id _ β) = id :=
  prod_id

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

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

Разделы

Аффилиация

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