map_coe_finRange — Mathlib

English

The elements of finRange n, viewed as Fin n, mapped by Fin.val yield the natural numbers 0,1,...,n−1: ((finRange n) : List (Fin n)).map Fin.val = List.range n.

Русский

Элементы finRange n, рассматриваемые как Fin n, отображаются через Fin.val в числа 0,1,...,n−1: ((finRange n) : List (Fin n)).map Fin.val = List.range n.

LaTeX

$$$$ \\text{List.map } Fin.val\\ (finRange\\ n) = \\text{List.range } n. $$$$

Lean4

@[simp]
theorem map_coe_finRange (n : ℕ) : ((finRange n) : List (Fin n)).map (Fin.val) = List.range n := by
  apply List.ext_getElem <;> simp

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