dropFun_prod

Mathlib.Data.TypeVec

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

English

Dropping the functor commutes with taking the product map.

Русский

dropFun commuting with prod.map

LaTeX

$$\operatorname{dropFun}(f \otimes' f') = (\operatorname{dropFun} f) \otimes' (\operatorname{dropFun} f')$$

Lean4

@[simp]
theorem dropFun_prod {α α' β β' : TypeVec (n + 1)} (f : α ⟹ β) (f' : α' ⟹ β') :
    dropFun (f ⊗' f') = (dropFun f ⊗' dropFun f') :=
  rfl

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

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

Разделы

Аффилиация

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