index_map_equiv

Mathlib.GroupTheory.Index

URI: https://scilib.ai/kg/mathlib#Subgroup.index_map_equiv

English

If e: G ≃* G' is a MulEquiv, then (map e H).index = H.index.

Русский

Если e: G ≃* G' — мультиэквив, то индекс образа H под e равен индексу H.

LaTeX

$$$ (\mathrm{map}\ e\ H).\mathrm{index} = H.\mathrm{index}. $$$

Lean4

@[to_additive (attr := simp)]
theorem index_map_equiv (e : G ≃* G') : (map (e : G →* G') H).index = H.index :=
  index_map_of_bijective e.bijective H

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

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

Разделы

Аффилиация

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