kerParam_range_le_centralizer

Mathlib.GroupTheory.Perm.Centralizer

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

← MathLib Explorer

English

The range of kerParam g is contained in the centralizer of g.

Русский

Образ kerParam g содержится в центральизаторе g.

LaTeX

$$(kerParam g).range ≤ Subgroup.centralizer { g }$$

Lean4

theorem kerParam_range_le_centralizer : (kerParam g).range ≤ Subgroup.centralizer { g } :=
  by
  rw [kerParam_range_eq]
  exact map_subtype_le (toPermHom g).ker

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

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

Разделы

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

Аффилиация

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