Lists of elements of Fin n

This file develops some results on finRange n.

@[simp]

theorem List.count_finRange {n : ℕ} (a : Fin n) : count a (finRange n) = 1

@[simp]

theorem List.idxOf_finRange {k : ℕ} (i : Fin k) : idxOf i (finRange k) = ↑i

@[deprecated List.finRange_eq_nil_iff (since := "2025-11-04")]

theorem List.finRange_eq_nil {n : ℕ} : finRange n = [] ↔ n = 0

Alias of List.finRange_eq_nil_iff.

@[deprecated List.map_get_finRange (since := "2025-11-04")]

theorem List.finRange_map_get {α : Type u_1} (l : List α) : map l.get (finRange l.length) = l

Alias of List.map_get_finRange.

@[deprecated List.map_getElem_finRange (since := "2025-11-04")]

theorem List.finRange_map_getElem {α : Type u_1} (l : List α) : map (fun (x : Fin l.length) => l[↑x]) (finRange l.length) = l

Alias of List.map_getElem_finRange.

@[deprecated List.map_coe_finRange_eq_range (since := "2025-11-04")]

theorem List.map_coe_finRange {n : ℕ} : map (fun (x : Fin n) => ↑x) (finRange n) = range n

Alias of List.map_coe_finRange_eq_range.

@[deprecated List.finRange_succ (since := "2025-10-10")]

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

theorem List.ofFn_eq_pmap {α : Type u} {n : ℕ} {f : Fin n → α} : ofFn f = pmap (fun (i : ℕ) (hi : i < n) => f ⟨i, hi⟩) (range n) ⋯

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

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

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

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

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

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