orbitZMultiplesEquiv — Mathlib

English

For u ∈ ℤˣ and z ∈ ℤ, (u^z)^(Int) = (u^(z)) in the additive cast; equivalently, the inverse relation holds with cast.

Русский

Для u ∈ ℤˣ и z ∈ ℤ верно симметрическое отношение между возведением и приведением.

LaTeX

$$$ \forall u \in \mathbb{Z}^{\times}, \forall z \in \mathbb{Z},\ (u^{z})^{\text{cast}} = u^{z} $$$

Lean4

/-- The orbit `(ℤ • a) +ᵥ b` is a cycle of order `minimalPeriod (a +ᵥ ·) b`. -/
noncomputable def _root_.AddAction.orbitZMultiplesEquiv {α β : Type*} [AddGroup α] (a : α) [AddAction α β] (b : β) :
    AddAction.orbit (zmultiples a) b ≃ ZMod (minimalPeriod (a +ᵥ ·) b) :=
  (AddAction.orbitEquivQuotientStabilizer (zmultiples a) b).trans (zmultiplesQuotientStabilizerEquiv a b).toEquiv

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