map_rootsOfUnity_eq_pow_self — Mathlib

English

For a map σ on roots of unity, there exists an exponent m such that σ(ζ) = ζ^m for the root ζ.

Русский

Для отображения σ на корни единицы существует показатель m, при котором σ(ζ) = ζ^m.

LaTeX

$$$\exists m\; \sigma(\zeta) = (\zeta)^m$ for some m$$

Lean4

theorem map_rootsOfUnity_eq_pow_self [FunLike F R R] [MonoidHomClass F R R] (σ : F) (ζ : rootsOfUnity k R) :
    ∃ m : ℕ, σ (ζ : Rˣ) = ((ζ : Rˣ) : R) ^ m :=
  by
  obtain ⟨m, hm⟩ := MonoidHom.map_cyclic (restrictRootsOfUnity σ k)
  rw [← restrictRootsOfUnity_coe_apply, hm, ← zpow_mod_orderOf, ←
    Int.toNat_of_nonneg (m.emod_nonneg (Int.natCast_ne_zero.mpr (pos_iff_ne_zero.mp (orderOf_pos ζ)))), zpow_natCast,
    rootsOfUnity.coe_pow]
  exact ⟨(m % orderOf ζ).toNat, rfl⟩

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