orbitZPowersEquiv_symm_apply — Mathlib

English

For any a,b and k ∈ Z, the symm apply of orbitZPowersEquiv gives a^k acting on b as the orbit element.

Русский

Для любых a,b и k ∈ Z, симметричное применение orbitZPowersEquiv даёт действие a^k на b как элемент орбиты.

LaTeX

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

Lean4

@[to_additive]
theorem orbitZPowersEquiv_symm_apply (k : ZMod (minimalPeriod (a • ·) b)) :
    (orbitZPowersEquiv a b).symm k = (⟨a, mem_zpowers a⟩ : zpowers a) ^ (cast k : ℤ) • ⟨b, mem_orbit_self b⟩ :=
  rfl

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