index_powMonoidHom_range — Mathlib

English

For a cyclic abelian group G and integer d, the index of the kernel of powMonoidHom d equals gcd(|G|, d).

Русский

Для циклической абелевой группы G и целого d индекс ядра powMonoidHom d равен gcd(|G|, d).

LaTeX

$$(powMonoidHom d).ker.index = (Nat.card G).gcd d$$

Lean4

@[to_additive]
theorem index_powMonoidHom_range [CommGroup G] [IsCyclic G] [Finite G] (d : ℕ) :
    (powMonoidHom d : G →* G).range.index = (Nat.card G).gcd d := by rw [Subgroup.index_range, card_powMonoidHom_ker]

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