zmultiplesQuotientStabilizerEquiv_symm_apply

English

For an action with stabilizer, the inverse quotient map sends an element n to cast(n) times the corresponding generator in zmultiples.

Русский

Для действия с стабилизатором обратная карта к кваситному делению отправляет элемент n в приведение n на множитель a внутри zmultiples.

LaTeX

$$$ (zmultiplesQuotientStabilizerEquiv\ a\ b)^{-1}(n) = (\operatorname{cast} n : \mathbb{Z}) \;\cdot\; \langle a, \mathrm{mem\_zmultiples}(a)\rangle $$$

Lean4

theorem zmultiplesQuotientStabilizerEquiv_symm_apply (n : ZMod (minimalPeriod (a +ᵥ ·) b)) :
    (zmultiplesQuotientStabilizerEquiv a b).symm n = (cast n : ℤ) • (⟨a, mem_zmultiples a⟩ : zmultiples a) :=
  rfl

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