index_smul

Mathlib.GroupTheory.Index

URI: https://scilib.ai/kg/mathlib#AddSubgroup.index_smul

English

For AddSubgroup S of an additive group with a G-action, (a • S).index = S.index for any a.

Русский

Для AddSubgroup S внутри аддитивной группы с действием G, для любого a выполняется (a • S).index = S.index.

LaTeX

$$(a • S).index = S.index$$

Lean4

@[simp]
theorem index_smul (a : G) (S : AddSubgroup A) : (a • S).index = S.index :=
  index_map_of_bijective (MulAction.bijective _) _

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

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

Разделы

Аффилиация

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