finEquivZPowers — Mathlib

English

The application of the finite-order equivalence sends the finite index n to the corresponding power x^n.

Русский

Применение конечной эквивалентности переводит индекс n в соответствующую степень x^n.

LaTeX

$$finEquivZPowers hx n = ⟨x^n, n, zpow_natCast x n⟩$$

Lean4

/-- The equivalence between `Fin (orderOf x)` and `Subgroup.zpowers x`, sending `i` to `x ^ i`. -/
@[to_additive /-- The equivalence between `Fin (addOrderOf a)` and
    `Subgroup.zmultiples a`, sending `i` to `i • a`. -/
    ]
noncomputable def finEquivZPowers (hx : IsOfFinOrder x) : Fin (orderOf x) ≃ zpowers x :=
  (finEquivPowers hx).trans <| Equiv.setCongr hx.powers_eq_zpowers

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