decomposeFin_symm_apply_zero

Mathlib.GroupTheory.Perm.Fin

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.decomposeFin_symm_apply_zero

← MathLib Explorer

English

For any p ∈ Fin(n+1) and e ∈ Perm(Fin n), the value of decomposeFin.symm(p,e) at 0 is p.

Русский

Для любых p ∈ Fin(n+1) и e ∈ Perm(Fin n) значение decomposeFin.symm(p,e) в 0 равно p.

LaTeX

$$$ \\mathrm{decomposeFin.symm}(p, e)(0) = p$$$

Lean4

@[simp]
theorem decomposeFin_symm_apply_zero {n : ℕ} (p : Fin (n + 1)) (e : Perm (Fin n)) :
    Equiv.Perm.decomposeFin.symm (p, e) 0 = p := by simp [Equiv.Perm.decomposeFin]

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

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

Разделы

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

Аффилиация

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