Documentation

Mathlib.Data.List.FinRange

Lists of elements of Fin n #

This file develops some results on finRange n.

@[simp]
theorem List.finRange_succ (n : ) :
List.finRange n.succ = (List.map Fin.castSucc (List.finRange n)).concat (Fin.last n)
theorem List.ofFn_eq_pmap {α : Type u} {n : } {f : Fin nα} :
List.ofFn f = List.pmap (fun (i : ) (hi : i < n) => f i, hi) (List.range n)
theorem List.ofFn_eq_map {α : Type u} {n : } {f : Fin nα} :
theorem List.nodup_ofFn_ofInjective {α : Type u} {n : } {f : Fin nα} (hf : Function.Injective f) :
(List.ofFn f).Nodup
theorem List.nodup_ofFn {α : Type u} {n : } {f : Fin nα} :
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.