card_powMonoidHom_range — Mathlib

English

For a cyclic finite group G and any d, the range of the d-th power monoid hom has cardinal equal to |G| / gcd(|G|, d).

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem card_powMonoidHom_range [CommGroup G] [hG : IsCyclic G] [Finite G] (d : ℕ) :
    Nat.card (powMonoidHom d : G →* G).range = Nat.card G / (Nat.card G).gcd d :=
  by
  obtain ⟨g, h⟩ := isCyclic_iff_exists_zpowers_eq_top.mp hG
  rw [MonoidHom.range_eq_map, ← h, MonoidHom.map_zpowers, Nat.card_zpowers, powMonoidHom_apply, orderOf_pow,
    orderOf_eq_card_of_zpowers_eq_top h]

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