etaExpand_eq

Mathlib.Data.Fin.Tuple.Reflection

URI: https://scilib.ai/kg/mathlib#FinVec.etaExpand_eq

← MathLib Explorer

English

Eta-expand yields the original vector: etaExpand(v) = v.

Русский

Эта-expand даёт исходный вектор: etaExpand(v) = v.

LaTeX

$$$\eta\text{Expand}(v) = v$$$

Lean4

/-- This can be used to prove
```lean
example (a : Fin 2 → α) : a = ![a 0, a 1] :=
  (etaExpand_eq _).symm
```
-/
@[simp]
theorem etaExpand_eq {m} (v : Fin m → α) : etaExpand v = v :=
  map_eq id v

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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