card_map_dvd

Mathlib.GroupTheory.Index

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

← MathLib Explorer

English

For a subgroup H and a homomorphism f, Nat.card (H.map f) divides Nat.card H.

Русский

Для подгруппы H и гомоморфизма f число Nat.card (H.map f) делится на Nat.card H.

LaTeX

$$$ |H.map f| \mid |H|. $$$

Lean4

@[to_additive]
theorem card_map_dvd (f : G →* G') : Nat.card (H.map f) ∣ Nat.card H :=
  card_dvd_of_surjective (f.subgroupMap H) (f.subgroupMap_surjective H)

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

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

Разделы

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

Аффилиация

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