autEquivZmod_symm_apply_intCast — Mathlib

English

Inverse of autEquivZmod applied to an integer cast corresponds to ζ^m acting on α: (autZmod)^{-1}(m) α = ζ^m α.

Русский

Обратное к autEquivZmod применяемое к целому числу даёт действие ζ^m на α.

LaTeX

$$$ (\mathrm{autEquivZmod}(H,L,hζ))^{-1}(\mathrm{Multiplicative.ofAdd}(m))\, α = ζ^m \cdot α. $$$

Lean4

theorem autEquivZmod_symm_apply_intCast [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) (m : ℤ) :
    (autEquivZmod H L hζ).symm (Multiplicative.ofAdd (m : ZMod n)) α = ζ ^ m • α :=
  by
  have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
  rw [← autEquivRootsOfUnity_smul ⟨ζ, (mem_primitiveRoots hn).mpr hζ⟩ H L hα]
  simp [MulEquiv.subgroupCongr_symm_apply, Subgroup.smul_def, Units.smul_def, autEquivZmod]

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