zpowersQuotientStabilizerEquiv — Mathlib

English

There is a multiplicative equivalence between the quotient zpowers a ⧸ stabilizer(zpowers a) b and ZMod(minimalPeriod(a•·) b).

Русский

Существует мультипликативное эквивалентство между факторгруппой zpowers a ⧸ stabilizer(zpowers a) b и ZMod(minimalPeriod(a•·) b).

LaTeX

$$$ zpowers\, a \\coloneqq \\text{stabilizer}(zpowers(a))\\; b \\;\\cong_*\\; ZMod(\\minPeriod(a \\cdot \\cdot) b) $$$

Lean4

/-- The quotient `(a ^ ℤ) ⧸ (stabilizer b)` is cyclic of order `minimalPeriod ((•) a) b`. -/
noncomputable def zpowersQuotientStabilizerEquiv :
    zpowers a ⧸ stabilizer (zpowers a) b ≃* Multiplicative (ZMod (minimalPeriod (a • ·) b)) :=
  letI f := zmultiplesQuotientStabilizerEquiv (Additive.ofMul a) b
  AddEquiv.toMultiplicative f

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