# Lists of elements of Fin n#

This file develops some results on finRange n.

@[simp]
theorem List.map_coe_finRange (n : ) :
List.map Fin.val =
theorem List.finRange_succ_eq_map (n : ) :
List.finRange n.succ = 0 :: List.map Fin.succ
theorem List.finRange_succ (n : ) :
List.finRange n.succ = (List.map Fin.castSucc ).concat (Fin.last n)
theorem List.ofFn_eq_pmap {α : Type u} {n : } {f : Fin nα} :
= List.pmap (fun (i : ) (hi : i < n) => f i, hi) (List.range n)
theorem List.ofFn_id (n : ) :
theorem List.ofFn_eq_map {α : Type u} {n : } {f : Fin nα} :
=
theorem List.nodup_ofFn_ofInjective {α : Type u} {n : } {f : Fin nα} (hf : ) :
(List.ofFn f).Nodup
theorem List.nodup_ofFn {α : Type u} {n : } {f : Fin nα} :
(List.ofFn f).Nodup
theorem Equiv.Perm.map_finRange_perm {n : } (σ : Equiv.Perm (Fin n)) :
(List.map (⇑σ) ).Perm
theorem Equiv.Perm.ofFn_comp_perm {n : } {α : Type u} (σ : Equiv.Perm (Fin n)) (f : Fin nα) :
(List.ofFn (f σ)).Perm (List.ofFn f)

The list obtained from a permutation of a tuple f is permutation equivalent to the list obtained from f.