finiteIndex_ker

Mathlib.GroupTheory.Index

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

← MathLib Explorer

English

If the image of f is finite, then ker f has finite index in G.

Русский

Если образ f конечен, то ядро f имеет конечный индекс в G.

LaTeX

$$f.ker.FiniteIndex$$

Lean4

@[to_additive]
instance finiteIndex_ker {G' : Type*} [Group G'] (f : G →* G') [Finite f.range] : f.ker.FiniteIndex :=
  @finiteIndex_of_finite_quotient G _ f.ker (Finite.of_equiv f.range (QuotientGroup.quotientKerEquivRange f).symm)

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

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

Разделы

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

Аффилиация

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