Theorems · Theorem · combinatorics

Fin.insertNth_rev

∀ {n : ℕ} {α : Sort u_3} (i : Fin (n + 1)) (a : α) (f : Fin n → α) (j : Fin (n + 1)),
  i.insertNth a f j.rev = i.rev.insertNth a (f ∘ Fin.rev) j

Defined in

Mathlib.Data.Fin.Tuple.Basic

Cited by

3 results in Mathlib

Foundations

Depth 55 from the axioms · uses propext, Classical.choice, Quot.sound