snoc_castSucc

Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

URI: https://scilib.ai/kg/mathlib#SubMulAction.ofStabilizer.snoc_castSucc

English

For any x, and i ∈ Fin n, snoc x (i.castSucc) = x i.

Русский

Для любого x и i ∈ Fin n, snoc x (i.castSucc) = x i.

LaTeX

$$$ (\\mathrm{snoc}\\,x)(i^{\\mathrm{castSucc}}) = x(i). $$$

Lean4

@[to_additive]
theorem snoc_castSucc {n : ℕ} (x : Fin n ↪ ofStabilizer G a) (i : Fin n) : snoc x i.castSucc = x i := by simp [snoc]

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

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

Разделы

Аффилиация

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