index_powMonoidHom_ker — Mathlib

English

For cyclic finite G and d, the size of the kernel of powMonoidHom G d equals gcd(|G|, d).

Русский

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

LaTeX

$$Nat.card (powMonoidHom d : G →* G).ker = Nat.gcd (Nat.card G) d$$

Lean4

@[to_additive]
theorem index_powMonoidHom_ker [CommGroup G] [IsCyclic G] [Finite G] (d : ℕ) :
    (powMonoidHom d : G →* G).ker.index = Nat.card G / (Nat.card G).gcd d := by
  rw [Subgroup.index_ker, card_powMonoidHom_range]

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