autEquivZmod_symm_apply_natCast — Mathlib

English

Symmetric version with int-cast: the action on α respects the Z/nZ-symmetry up to the primitive root ζ.

Русский

Симметричная версия относительно целочисленного приведения: действие на α совместимо с симметрией Z/nZ и ζ.

LaTeX

$$$\text{autEquivZmod}(H,L,hζ)\,\text{symm}\; (\mathrm{Multiplicative.ofAdd}(m)) \ α = ζ^m α.$$$

Lean4

theorem autEquivZmod_symm_apply_natCast [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) (m : ℕ) :
    (autEquivZmod H L hζ).symm (Multiplicative.ofAdd (m : ZMod n)) α = ζ ^ m • α := by
  simpa only [Int.cast_natCast, zpow_natCast] using autEquivZmod_symm_apply_intCast H L hα hζ m

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