orbitZPowersEquiv_symm_apply' — Mathlib

English

There exists a symmetric variant: (orbitZPowersEquiv a b)^{-1}(k) = a^k • b in the zpowers orbit.

Русский

Существует симметричный вариант: (orbitZPowersEquiv a b)^{-1}(k) = a^k • b в орбите zpowers.

LaTeX

$$$ (\mathrm{orbitZPowersEquiv}\ a\ b)^{-1}(k) = a^{k} \cdot b $$$

Lean4

theorem orbitZPowersEquiv_symm_apply' (k : ℤ) :
    (orbitZPowersEquiv a b).symm k = (⟨a, mem_zpowers a⟩ : zpowers a) ^ k • ⟨b, mem_orbit_self b⟩ :=
  by
  rw [orbitZPowersEquiv_symm_apply, ZMod.coe_intCast]
  exact Subtype.ext (zpow_smul_mod_minimalPeriod _ _ k)

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