coe_autToPow_apply — Mathlib

English

For any automorphism f, the same equality as above holds in the target structure, aligning μ under f with the corresponding root-of-unity power.

Русский

Для любого автоморфизма f верно аналогичное равенство, согласующее образ μ под f с соответствующей степенью корня единицы.

LaTeX

$$$(autToPow R hμ f : ZMod n) = (map_rootsOfUnity_eq_pow_self f hμ.toRootsOfUnity).choose$$$

Lean4

theorem coe_autToPow_apply [NeZero n] (f : S ≃ₐ[R] S) :
    (autToPow R hμ f : ZMod n) = ((map_rootsOfUnity_eq_pow_self f hμ.toRootsOfUnity).choose : ZMod n) :=
  rfl

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