English
The automorphism-to-power construction is a noncomputable MonoidHom sending each automorphism to a unit in ZMod n, determined by how it maps the primitive root μ to a power of μ in the roots of unity.
Русский
Конструкция перехода автоморфизм → степень задаёт моноид-гомоморфизм, отображающий автоморфизм в единицу в ZMod n и задаваемый тем, как он отображает примитивный корень μ в степень μ в корнях единицы.
LaTeX
$$IsPrimitiveRoot.autToPow R hμ : (S ≃ₐ[R] S) →* (ZMod n)ˣ$$
Lean4
@[simp]
theorem autToPow_spec [NeZero n] (f : S ≃ₐ[R] S) : μ ^ (hμ.autToPow R f : ZMod n).val = f μ :=
by
rw [IsPrimitiveRoot.coe_autToPow_apply]
generalize_proofs h
refine (?_ : ((hμ.toRootsOfUnity : Sˣ) : S) ^ _ = _).trans h.choose_spec.symm
rw [← rootsOfUnity.coe_pow, ← rootsOfUnity.coe_pow]
congr 2
rw [pow_eq_pow_iff_modEq, ZMod.val_natCast]
conv => enter [2, 2]; rw [hμ.eq_orderOf]
rw [← Subgroup.orderOf_coe, ← orderOf_units]
exact Nat.mod_modEq _ _
