orbitZMultiplesEquiv_symm_apply' — Mathlib

English

The inverse of orbitZPowersEquiv applied to an integer k yields a power of a acting on b.

Русский

Обратное применение orbitZPowersEquiv для целого k даёт степень a, действующую на b.

LaTeX

$$$ (\mathrm{orbitZPowersEquiv}\ a\ b)^{-1}(k) = (\langle a, mem\_zpowers(a) \rangle)^{k} \cdot \langle b, mem\_orbit\_self(b) \rangle $$$

Lean4

theorem _root_.AddAction.orbitZMultiplesEquiv_symm_apply' {α β : Type*} [AddGroup α] (a : α) [AddAction α β] (b : β)
    (k : ℤ) :
    (AddAction.orbitZMultiplesEquiv a b).symm k =
      k • (⟨a, mem_zmultiples a⟩ : zmultiples a) +ᵥ ⟨b, AddAction.mem_orbit_self b⟩ :=
  by
  rw [AddAction.orbitZMultiplesEquiv_symm_apply, ZMod.coe_intCast]
    -- Making `a` explicit turns this from ~190000 heartbeats to ~700.

  exact Subtype.ext (zsmul_vadd_mod_minimalPeriod a _ k)

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