card_range_dvd

Mathlib.GroupTheory.Index

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

← MathLib Explorer

English

For any f: G →* G', Nat.card (im f) divides Nat.card G.

Русский

Для любого f: G →* G' число Nat.card (образ f) делит Nat.card G.

LaTeX

$$$ |\mathrm{im}(f)| \mid |G|. $$$

Lean4

@[to_additive]
theorem card_range_dvd (f : G →* G') : Nat.card f.range ∣ Nat.card G :=
  card_dvd_of_surjective f.rangeRestrict f.rangeRestrict_surjective

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

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

Разделы

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

Аффилиация

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