quotientEquivSigmaZMod_apply — Mathlib

English

The forward action of quotientEquivSigmaZMod sends g^k • q.out to ⟨q,k⟩.

Русский

Стандартное применение quotientEquivSigmaZMod отправляет g^k • q.out в ⟨q,k⟩.

LaTeX

$$$ quotientEquivSigmaZMod H g \; (g^k \cdot q.out) = \langle q, k \rangle $$$

Lean4

theorem quotientEquivSigmaZMod_apply (q : orbitRel.Quotient (zpowers g) (G ⧸ H)) (k : ℤ) :
    quotientEquivSigmaZMod H g (g ^ k • q.out) = ⟨q, k⟩ := by
  rw [apply_eq_iff_eq_symm_apply, quotientEquivSigmaZMod_symm_apply, ZMod.coe_intCast, zpow_smul_mod_minimalPeriod]

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