insertNth_comp_cycleRange_symm

Mathlib.GroupTheory.Perm.Fin

URI: https://scilib.ai/kg/mathlib#Fin.insertNth_comp_cycleRange_symm

← MathLib Explorer

English

The composition of p.insertNth a x with p.cycleRange.symm equals Fin.cons a x.

Русский

Составление p.insertNth a x с p.cycleRange.symm даёт Fin.cons a x.

LaTeX

$$$(p.insertNth\ a\ x) \circ p.cycleRange^{-1} = \mathrm{Fin}.cons\ a\ x$$$

Lean4

@[simp]
theorem insertNth_comp_cycleRange_symm {α : Type*} (p : Fin (n + 1)) (a : α) (x : Fin n → α) :
    (p.insertNth a x ∘ p.cycleRange.symm : _ → α) = Fin.cons a x :=
  by
  ext j
  simp

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru