quotientEquivSigmaZMod_symm_apply

English

In the quotient SigmaZMod associated to a subgroup H of G and a generator g, the inverse image of a pair ⟨q, k⟩ under the symmetry map is g^k acting on the representative q.out.

Русский

В кванте SigmaZMod, связанной с подгруппой H внутри G и элементом-генератором g, обратное образующее пары ⟨q, k⟩ под симметричной картой равно g^k, действующему на представителя q.out.

LaTeX

$$$ (\\text{quotientEquivSigmaZMod } H\\, g).{\\rm symm}^{-1} \\langle q, k \\rangle = g^{(cast\\ k : \\mathbb{Z})} \\cdot q.out $$$

Lean4

theorem quotientEquivSigmaZMod_symm_apply (q : orbitRel.Quotient (zpowers g) (G ⧸ H))
    (k : ZMod (minimalPeriod (g • ·) q.out)) : (quotientEquivSigmaZMod H g).symm ⟨q, k⟩ = g ^ (cast k : ℤ) • q.out :=
  rfl

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