English
There is a canonical equivalence between Fin(orderOf x) and powers x.
Русский
Существует каноническое биективное соответствие между Fin(orderOf x) и powers x.
LaTeX
$$finEquivPowers(x) : \mathrm{Fin}(\operatorname{orderOf}(x)) \simeq \mathrm{powers}(x)$$
Lean4
/-- The equivalence between `Fin (orderOf x)` and `Submonoid.powers x`, sending `i` to `x ^ i` -/
@[to_additive /-- The equivalence between `Fin (addOrderOf a)` and
`AddSubmonoid.multiples a`, sending `i` to `i • a` -/
]
noncomputable def finEquivPowers {x : G} (hx : IsOfFinOrder x) : Fin (orderOf x) ≃ powers x :=
Equiv.ofBijective (fun n ↦ ⟨x ^ (n : ℕ), ⟨n, rfl⟩⟩)
⟨fun ⟨_, h₁⟩ ⟨_, h₂⟩ ij ↦ Fin.ext (pow_injOn_Iio_orderOf h₁ h₂ (Subtype.mk_eq_mk.1 ij)), fun ⟨_, i, rfl⟩ ↦
⟨⟨i % orderOf x, mod_lt _ hx.orderOf_pos⟩, Subtype.eq <| pow_mod_orderOf _ _⟩⟩
