dropFun_diag

Mathlib.Data.TypeVec

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

English

Dropping the functor from the diagonal object yields the diagonal again.

Русский

Уменьшая размерность применением dropFun к диагонали, получаем диагональ заново.

LaTeX

$$\operatorname{dropFun}(\operatorname{prod.diag}) = \operatorname{prod.diag}$$

Lean4

@[simp]
theorem dropFun_diag {α} : dropFun (@prod.diag (n + 1) α) = prod.diag :=
  rfl

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

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

Разделы

Аффилиация

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