card_mulAut — Mathlib

English

The cardinality of MulAut G equals the Euler totient of |G| for cyclic finite G.

Русский

Множество автоморфизмов циклической конечной группы имеет размер φ(|G|).

LaTeX

$$Nat.card (MulAut G) = Nat.totient (Nat.card G) for [Finite G] and [IsCyclic G].$$

Lean4

theorem card_mulAut [Group G] [Finite G] [h : IsCyclic G] : Nat.card (MulAut G) = Nat.totient (Nat.card G) :=
  by
  have : NeZero (Nat.card G) := ⟨Nat.card_pos.ne'⟩
  rw [← ZMod.card_units_eq_totient, ← Nat.card_eq_fintype_card]
  exact Nat.card_congr (mulAutMulEquiv G)

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