English
There is a canonical monoid homomorphism from the automorphism group of S over R to the unit group of Z/nZ, sending each automorphism to the power by which it maps the primitive root μ to μ under the automorphism.
Русский
Существуют канонические гомоморфизм моноидов от группы автоморфизмов S над R к группе единиц Z/nZ, отправляющий каждый автоморфизм в показатель степени, на который μ отображается под этим автоморфизмом.
LaTeX
$$$\mathrm{autToPow}\;R\;h\mu : (S \simeq_R S) \to (\mathbb{Z}/n\mathbb{Z})^{\times}$$$
Lean4
theorem _root_.card_rootsOfUnity_eq_iff_exists_isPrimitiveRoot {n : ℕ} [NeZero n] :
Fintype.card (rootsOfUnity n R) = n ↔ ∃ ζ : R, IsPrimitiveRoot ζ n :=
by
refine ⟨fun h ↦ ?_, fun ⟨ζ, hζ⟩ ↦ hζ.card_rootsOfUnity⟩
obtain ⟨⟨ζ, hζ'⟩, hζ⟩ := (rootsOfUnity.isCyclic R n).exists_ofOrder_eq_natCard
rw [Nat.card_eq_fintype_card, h, ← IsPrimitiveRoot.iff_orderOf, ← coe_submonoidClass_iff, ←
IsPrimitiveRoot.coe_units_iff] at hζ
use ζ
