finEquivPowers_symm_apply — Mathlib

English

The inverse map sends a power x^n back to n modulo orderOf x.

Русский

Обратное отображение возвращает x^n к числу n по модулю orderOf(x).

LaTeX

$$(finEquivPowers(hx)).symm(⟨x^{n}, _, rfl⟩) = ⟨n \bmod \operatorname{orderOf}(x), \mathrm{mod\;lt}\, \operatorname{orderOf}(x)\rangle$$

Lean4

@[to_additive (attr := simp)]
theorem finEquivPowers_symm_apply {x : G} (hx : IsOfFinOrder x) (n : ℕ) :
    (finEquivPowers hx).symm ⟨x ^ n, _, rfl⟩ = ⟨n % orderOf x, Nat.mod_lt _ hx.orderOf_pos⟩ := by
  rw [Equiv.symm_apply_eq, finEquivPowers_apply, Subtype.mk_eq_mk, ← pow_mod_orderOf, Fin.val_mk]

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