Documentation

Mathlib.Data.List.FinRange

Lists of elements of Fin n #

This file develops some results on finRange n.

@[simp]
theorem List.ofFn_eq_pmap {α : Type u_1} {n : } {f : Fin nα} :
List.ofFn f = List.pmap (fun i hi => f { val := i, isLt := hi }) (List.range n) (_ : ∀ (x : ), x List.range nx < n)
theorem List.ofFn_eq_map {α : Type u_1} {n : } {f : Fin nα} :
theorem List.nodup_ofFn_ofInjective {α : Type u_1} {n : } {f : Fin nα} (hf : Function.Injective f) :
theorem List.nodup_ofFn {α : Type u_1} {n : } {f : Fin nα} :
theorem Equiv.Perm.ofFn_comp_perm {n : } {α : Type u} (σ : Equiv.Perm (Fin n)) (f : Fin nα) :
List.ofFn (f σ) ~ List.ofFn f

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