index_zmultiples

Mathlib.Data.ZMod.QuotientGroup

URI: https://scilib.ai/kg/mathlib#Int.index_zmultiples

← MathLib Explorer

English

The index of the subgroup zmultiples(a) equals a.natAbs.

Русский

Индекс подпгруппы zmultiples(a) равен a.natAbs.

LaTeX

$$$ \operatorname{index}(\mathrm{zmultiples}(a)) = a.natAbs $$$

Lean4

@[simp]
theorem index_zmultiples (a : ℤ) : (AddSubgroup.zmultiples a).index = a.natAbs := by
  rw [AddSubgroup.index, Nat.card_congr (quotientZMultiplesEquivZMod a).toEquiv, Nat.card_zmod]

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

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

Разделы

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

Аффилиация

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