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 (List.finRange n) = List.range n

theorem List.finRange_succ_eq_map (n : ℕ) : List.finRange (Nat.succ n) = 0 :: List.map Fin.succ (List.finRange n)

theorem List.finRange_succ (n : ℕ) : List.finRange (Nat.succ n) = List.concat (List.map Fin.castSucc (List.finRange n)) (Fin.last n)

theorem List.ofFn_eq_pmap {α : Type u_1} {n : ℕ} {f : Fin n → α} : List.ofFn f = List.pmap (fun (i : ℕ) (hi : i < n) => f { val := i, isLt := hi }) (List.range n) (_ : ∀ x ∈ List.range n, x < n)

theorem List.ofFn_id (n : ℕ) : List.ofFn id = List.finRange n

theorem List.ofFn_eq_map {α : Type u_1} {n : ℕ} {f : Fin n → α} : List.ofFn f = List.map f (List.finRange n)

theorem List.nodup_ofFn_ofInjective {α : Type u_1} {n : ℕ} {f : Fin n → α} (hf : Function.Injective f) : List.Nodup (List.ofFn f)

theorem List.nodup_ofFn {α : Type u_1} {n : ℕ} {f : Fin n → α} : List.Nodup (List.ofFn f) ↔ Function.Injective f

theorem Equiv.Perm.map_finRange_perm {n : ℕ} (σ : Equiv.Perm (Fin n)) : List.Perm (List.map (⇑σ) (List.finRange n)) (List.finRange n)

theorem Equiv.Perm.ofFn_comp_perm {n : ℕ} {α : Type u} (σ : Equiv.Perm (Fin n)) (f : Fin n → α) : List.Perm (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.