reindex_apply

Mathlib.GroupTheory.FreeGroup.IsFreeGroup

URI: https://scilib.ai/kg/mathlib#FreeGroupBasis.reindex_apply

English

Reindexing a basis by e yields the same evaluation on indices after applying e.

Русский

Переиндексация базиса по e сохраняет значения индексов после применения e.

LaTeX

$$$$ b.reindex\\, e \\; x = b( e^{-1}(x) ). $$$$

Lean4

@[simp]
theorem reindex_apply (b : FreeGroupBasis ι G) (e : ι ≃ ι') (x : ι') : b.reindex e x = b (e.symm x) :=
  rfl

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

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

Разделы

Аффилиация

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